glb_Ioi_eq_self_or_Ioi_eq_Ici — Mathlib

English

Let γ be a partially ordered set. For any i ∈ γ, if j is the greatest lower bound of the set { x ∈ γ | x > i }, then either j = i or Ioi(i) = Ici(j).

Русский

Пусть γ — частично упорядоченное множество. Пусть i ∈ γ. Если j является наибольшей нижней гранью множества { x ∈ γ | x > i }, то либо j = i, либо Ioi(i) = Ici(j).

LaTeX

$$$ IsGLB(Ioi(i)) j \rightarrow (j = i) \lor (Ioi(i) = Ici(j)). $$$

Lean4

theorem glb_Ioi_eq_self_or_Ioi_eq_Ici [PartialOrder γ] {j : γ} (i : γ) (hj : IsGLB (Ioi i) j) : j = i ∨ Ioi i = Ici j :=
  @lub_Iio_eq_self_or_Iio_eq_Iic γᵒᵈ _ j i hj

Похожие утверждения