lub_Iio_eq_self_or_Iio_eq_Iic — Mathlib

English

For a partial order, if j is LUB of Iio i, then either j = i or Iio i = Iic j.

Русский

Для частичного порядка, если j является наим. верхней границей множества Iio i, тогда либо j = i, либо Iio i равно Iic j.

LaTeX

$$$[PartialOrder γ] \; {i j : γ} (IsLUB(Iio(i), j) \Rightarrow (j = i) \lor (Iio(i) = Iic(j)))$$$

Lean4

theorem lub_Iio_eq_self_or_Iio_eq_Iic [PartialOrder γ] {j : γ} (i : γ) (hj : IsLUB (Iio i) j) : j = i ∨ Iio i = Iic j :=
  by
  rcases eq_or_lt_of_le (lub_Iio_le i hj) with hj_eq_i | hj_lt_i
  · exact Or.inl hj_eq_i
  · right
    exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

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