def irreflexivize {α : Sort u_1} (R : α → α → Prop) (x : α) (y : α) : Prop

Equations

• R⁻ʳ x y = (x ≠ y ∧ R x y)

def «term_⁻ʳ» : Lean.TrailingParserDescr

Equations

• «term_⁻ʳ» = Lean.ParserDescr.trailingNode `term_⁻ʳ 1024 1024 (Lean.ParserDescr.symbol "⁻ʳ")

@[reducible, inline]

abbrev WeaklyConverseWellFounded {α : Type u_1} (R : α → α → Prop) : Prop

Equations

• WeaklyConverseWellFounded R = ConverseWellFounded R⁻ʳ

theorem dependent_choice {α : Type u_1} {R : α → α → Prop} (h : ∃ (s : Set α), s.Nonempty ∧ ∀ a ∈ s, ∃ b ∈ s, R a b) : ∃ (f : ℕ → α), ∀ (x : ℕ), R (f x) (f (x + 1))

theorem antisymm_of_WCWF : ∀ {α : Type u_1} {R : α → α → Prop}, WeaklyConverseWellFounded R → Antisymmetric R

theorem Finite.exists_ne_map_eq_of_infinite_lt {α : Type u_1} {β : Sort u_2} [LinearOrder α] [Infinite α] [Finite β] (f : α → β) : ∃ (x : α) (y : α), x < y ∧ f x = f y

theorem WCWF_of_antisymm_trans {α : Type u_1} {R : α → α → Prop} (hFin : Finite α) (R_trans : Transitive R) : Antisymmetric R → WeaklyConverseWellFounded R

theorem LO.Modal.Standard.Kripke.axiomT_defines {α : Type u} [Inhabited α] : LO.Modal.Standard.AxiomSet.DefinesKripkeFrameClass 𝗧 LO.Modal.Standard.Kripke.ReflexiveFrameClass

theorem LO.Modal.Standard.Kripke.axiomFour_defines {α : Type u} [Inhabited α] : LO.Modal.Standard.AxiomSet.DefinesKripkeFrameClass 𝟰 LO.Modal.Standard.Kripke.TransitiveFrameClass

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass : LO.Modal.Standard.Kripke.FrameClass

Equations

• LO.Modal.Standard.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass F = (Reflexive F.Rel ∧ Transitive F.Rel ∧ WeaklyConverseWellFounded F.Rel)

theorem LO.Modal.Standard.Kripke.axiomGrz_defines {α : Type u} [Inhabited α] [DecidableEq α] : LO.Modal.Standard.AxiomSet.DefinesKripkeFrameClass 𝗚𝗿𝘇 LO.Modal.Standard.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.ReflexiveTransitiveAntisymmetricFrameClass : LO.Modal.Standard.Kripke.FrameClass

Equations

• LO.Modal.Standard.Kripke.ReflexiveTransitiveAntisymmetricFrameClass F = (Reflexive F.Rel ∧ Transitive F.Rel ∧ Antisymmetric F.Rel)

theorem LO.Modal.Standard.Kripke.axiomGrz_finite_defines {α : Type u} [Inhabited α] [DecidableEq α] : LO.Modal.Standard.AxiomSet.FinitelyDefinesKripkeFrameClass 𝗚𝗿𝘇 LO.Modal.Standard.Kripke.ReflexiveTransitiveAntisymmetricFrameClass.toFiniteFrameClass

instance LO.Modal.Standard.Kripke.Grz_sound {α : Type u} [Inhabited α] [DecidableEq α] : LO.Sound 𝐆𝐫𝐳 LO.Modal.Standard.Kripke.ReflexiveTransitiveAntisymmetricFrameClassꟳ.alt

Equations

• ⋯ = ⋯

instance LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterGrz {α : Type u} [Inhabited α] [DecidableEq α] : LO.System.Consistent 𝐆𝐫𝐳

Equations

• ⋯ = ⋯