Icc_ssubset_Icc_right — Mathlib

English

If a2 ≤ b2, a2 ≤ a1 and b1 < b2, then Icc(a1,b1) ⊂ 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_right (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) : Icc a₁ b₁ ⊂ Icc a₂ b₂ :=
  (ssubset_iff_of_subset (Icc_subset_Icc ha (le_of_lt hb))).mpr
    ⟨b₂, right_mem_Icc.mpr hI, fun f => lt_irrefl b₁ (hb.trans_le f.2)⟩

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