Ici_ssubset_Ici — Mathlib

English

Ici(a) is a proper subset of Ici(b) iff b < a.

Русский

Ici(a) является строгим подмножеством Ici(b) тогда и только тогда, когда b < a.

LaTeX

$$$ \mathrm{Ici}(a) \subsetneq \mathrm{Ici}(b) \iff b < a $$$

Lean4

@[simp]
theorem Ici_ssubset_Ici : Ici a ⊂ Ici b ↔ b < a
    where
  mp
    h := by
    obtain ⟨ab, c, cb, ac⟩ := ssubset_iff_exists.mp h
    exact lt_of_le_not_ge (Ici_subset_Ici.mp ab) (fun h' ↦ ac (h'.trans cb))
  mpr h := (ssubset_iff_of_subset (Ici_subset_Ici.mpr h.le)).mpr ⟨b, right_mem_Iic, fun h' => h.not_ge h'⟩

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