Icc_ssubset_Icc_left — Mathlib

English

If a2 ≤ b2 and a2 < a1 and b1 ≤ b2, then Icc(a1,b1) is strictly contained in Icc(a2,b2).

Русский

Если a2 ≤ b2 и a2 < a1 и b1 ≤ b2, то Icc(a1,b1) ⊂ Icc(a2,b2).

LaTeX

$$$$Icc(a_1,b_1) \subset Icc(a_2,b_2)$$$$

Lean4

theorem Icc_ssubset_Icc_left (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊂ Icc a₂ b₂ :=
  (ssubset_iff_of_subset (Icc_subset_Icc (le_of_lt ha) hb)).mpr
    ⟨a₂, left_mem_Icc.mpr hI, not_and.mpr fun f _ => lt_irrefl a₂ (ha.trans_le f)⟩

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