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

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