Ici_eq_singleton_iff_isTop — Mathlib

English

The ray [x, ∞) is a singleton {x} exactly when x is a top element of the order.

Русский

Луч [x, ∞) является единичным множеством {x} тогда и только тогда x является наибольшим элементом порядка.

LaTeX

$$$ ( [x, \infty) = \{x\} ) \iff IsTop(x) $$$

Lean4

theorem Ici_eq_singleton_iff_isTop {x : α} : (Ici x = { x }) ↔ IsTop x :=
  by
  refine ⟨fun h y ↦ ?_, fun h ↦ by ext y; simp [(h y).ge_iff_eq]⟩
  by_contra! H
  have : y ∈ Ici x := H.le
  rw [h, mem_singleton_iff] at this
  exact lt_irrefl y (this.le.trans_lt H)

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