Icc_ssubset_Icc_left — Mathlib

English

If a2 ≤ b2, 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

$$$ (a_2 \le b_2) \land (a_2 < a_1) \land (b_1 \le b_2) \Rightarrow 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₂ :=
  by
  rw [← coe_ssubset, coe_Icc, coe_Icc]
  exact Set.Icc_ssubset_Icc_left hI ha hb

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