Icc_subset_Icc_iff — Mathlib

English

If a1 ≤ b1, then Icc(a1, b1) ⊆ Icc(a2, b2) holds if and only if a2 ≤ a1 and b1 ≤ b2.

Русский

Если a1 ≤ b1, то Icc(a1,b1) ⊆ Icc(a2,b2) тогда и только тогда, когда a2 ≤ a1 и b1 ≤ b2.

LaTeX

$$$ (a_1 \le b_1) \Rightarrow ( Icc(a_1,b_1) \subseteq Icc(a_2,b_2) \iff a_2 \le a_1 \land b_1 \le b_2 ) $$$

Lean4

theorem Icc_subset_Icc_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ := by
  rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]

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