Ioi_subset_Ici_iff — Mathlib

English

For densely ordered sets, Ioi b ⊆ Ici a iff a ≤ b.

Русский

Для плотно упорядоченных множеств Ioi b ⊆ Ici a тогда, когда a ≤ b.

LaTeX

$$$ Ioi(b) \subseteq Ici(a) \iff a \le b $ (dense order) $$

Lean4

@[simp]
theorem Ioi_subset_Ici_iff [DenselyOrdered α] : Ioi b ⊆ Ici a ↔ a ≤ b :=
  by
  refine ⟨fun h => ?_, Ioi_subset_Ici⟩
  by_contra ba
  obtain ⟨c, bc, ca⟩ : ∃ c, b < c ∧ c < a := exists_between (not_le.mp ba)
  exact lt_irrefl _ (ca.trans_le (h bc))

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