def
LO.FirstOrder.succInd
{L : LO.FirstOrder.Language}
[L.ORing]
{ΞΎ : Type u_3}
(p : LO.FirstOrder.Semiformula L ΞΎ 1)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.orderInd
{L : LO.FirstOrder.Language}
[L.ORing]
{ΞΎ : Type u_3}
(p : LO.FirstOrder.Semiformula L ΞΎ 1)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.leastNumber
{L : LO.FirstOrder.Language}
[L.ORing]
{ΞΎ : Type u_3}
(p : LO.FirstOrder.Semiformula L ΞΎ 1)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
- equal: β p β ππ, πβ p
- Ξ©β: β (n m : β), πβ (β(!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ n)) + !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ m))) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ (n + m)))β)
- Ξ©β: β (n m : β), πβ (β(!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ n)) * !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ m))) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ (n * m)))β)
- Ξ©β: β (n m : β), n β m β πβ (βΒ¬!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ n)) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ m))β)
- Ξ©β: β (n : β), πβ (ββ' (!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ n)) β !(LO.disjLt (fun (i : β) => β!!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ββα΅£ i))β) n))β)
Instances For
Equations
- LO.FirstOrder.Theory.Β«termπβΒ» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termπβ 1024 (Lean.ParserDescr.symbol "πβ")
Instances For
- equal: β p β ππ, ππβ» p
- addZero: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) + 0) = !!(LO.FirstOrder.Semiterm.fvar 0)β)
- addAssoc: ππβ» (β((!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.fvar 1)) + !!(LO.FirstOrder.Semiterm.fvar 2)) = (!!(LO.FirstOrder.Semiterm.fvar 0) + (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 2)))β)
- addComm: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.fvar 1)) = (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 0))β)
- addEqOfLt: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) β β' (!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.bvar 0)) = !!(LO.FirstOrder.Semiterm.fvar 1))β)
- zeroLe: ππβ» (β0 β€ !!(LO.FirstOrder.Semiterm.fvar 0)β)
- zeroLtOne: ππβ» (β0 < 1β)
- oneLeOfZeroLt: ππβ» (β(0 < !!(LO.FirstOrder.Semiterm.fvar 0) β 1 β€ !!(LO.FirstOrder.Semiterm.fvar 0))β)
- addLtAdd: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) β (!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.fvar 2)) < (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 2)))β)
- mulZero: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) * 0) = 0β)
- mulOne: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) * 1) = !!(LO.FirstOrder.Semiterm.fvar 0)β)
- mulAssoc: ππβ» (β((!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 1)) * !!(LO.FirstOrder.Semiterm.fvar 2)) = (!!(LO.FirstOrder.Semiterm.fvar 0) * (!!(LO.FirstOrder.Semiterm.fvar 1) * !!(LO.FirstOrder.Semiterm.fvar 2)))β)
- mulComm: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 1)) = (!!(LO.FirstOrder.Semiterm.fvar 1) * !!(LO.FirstOrder.Semiterm.fvar 0))β)
- mulLtMul: ππβ» (β((!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) β§ 0 < !!(LO.FirstOrder.Semiterm.fvar 2)) β (!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 2)) < (!!(LO.FirstOrder.Semiterm.fvar 1) * !!(LO.FirstOrder.Semiterm.fvar 2)))β)
- distr: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) * (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 2))) = ((!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 1)) + (!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 2)))β)
- ltIrrefl: ππβ» (βΒ¬!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 0)β)
- ltTrans: ππβ» (β((!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) β§ !!(LO.FirstOrder.Semiterm.fvar 1) < !!(LO.FirstOrder.Semiterm.fvar 2)) β !!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 2))β)
- ltTri: ππβ» (β(!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) β¨ (!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 1) β¨ !!(LO.FirstOrder.Semiterm.fvar 1) < !!(LO.FirstOrder.Semiterm.fvar 0)))β)
Instances For
Equations
- LO.FirstOrder.Theory.Β«termππβ»Β» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termππβ» 1024 (Lean.ParserDescr.symbol "ππβ»")
Instances For
def
LO.FirstOrder.Theory.indScheme
(L : LO.FirstOrder.Language)
[L.ORing]
(Ξ : LO.FirstOrder.Semiformula L β 1 β Prop)
:
Equations
- LO.FirstOrder.Theory.indScheme L Ξ = {q : LO.FirstOrder.SyntacticFormula L | β (p : LO.FirstOrder.Semiformula L β 1), Ξ p β§ q = LO.FirstOrder.succInd p}
Instances For
@[reducible, inline]
Equations
- πopen = ππβ» + LO.FirstOrder.Theory.indScheme ββα΅£ LO.FirstOrder.Semiformula.Open
Instances For
Equations
- LO.FirstOrder.Theory.Β«termπopenΒ» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termπopen 1024 (Lean.ParserDescr.symbol "πopen")
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.FirstOrder.Theory.Β«termπππ_Β» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termπππ_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "πππ") (Lean.ParserDescr.cat `term 1024))
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.FirstOrder.Theory.Β«termππΊ_Β» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termππΊ_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ππΊ") (Lean.ParserDescr.cat `term 1024))
Instances For
Equations
- LO.FirstOrder.Theory.Β«termππΊβΒ» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termππΊβ 1024 (Lean.ParserDescr.symbol "ππΊβ")
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.FirstOrder.Theory.Β«termππ·_Β» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termππ·_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ππ·") (Lean.ParserDescr.cat `term 1024))
Instances For
Equations
- LO.FirstOrder.Theory.Β«termππ·βΒ» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termππ·β 1024 (Lean.ParserDescr.symbol "ππ·β")
Instances For
Equations
- LO.FirstOrder.Theory.Β«termππΊβΒ» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termππΊβ 1024 (Lean.ParserDescr.symbol "ππΊβ")
Instances For
Equations
- LO.FirstOrder.Theory.Β«termππ·βΒ» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termππ·β 1024 (Lean.ParserDescr.symbol "ππ·β")
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.FirstOrder.Theory.Β«termππΒ» = Lean.ParserDescr.node `LO.FirstOrder.Theory.termππ 1024 (Lean.ParserDescr.symbol "ππ")
Instances For
theorem
LO.FirstOrder.Theory.coe_indH_subset_indH
{L : LO.FirstOrder.Language}
[L.ORing]
{Ξ : LO.Polarity}
{Ξ½ : β}
:
β(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) '' LO.FirstOrder.Theory.indScheme ββα΅£ (LO.FirstOrder.Arith.Hierarchy Ξ Ξ½) β LO.FirstOrder.Theory.indScheme L (LO.FirstOrder.Arith.Hierarchy Ξ Ξ½)
Equations
- LO.FirstOrder.Theory.PAMinus.subtheoryOfIndH = LO.System.Subtheory.ofSubset β―
instance
LO.FirstOrder.Theory.EQ.subtheoryOfIndH
{Ξ : LO.Polarity}
{n : β}
:
ππ βΌ πππΞ n
Equations
- LO.FirstOrder.Theory.EQ.subtheoryOfIndH = LO.FirstOrder.Theory.PAMinus.subtheoryOfIndH.comp LO.FirstOrder.Theory.EQ.subtheoryOfPAMinus
Equations
- LO.FirstOrder.Theory.EQ.subtheoryOfIOpen = inferInstance.comp LO.FirstOrder.Theory.EQ.subtheoryOfPAMinus