Icc_subset_Icc_iff — Mathlib

English

For any a1 ≤ b1, Icc(a1,b1) ⊆ Icc(a2,b2) holds if and only if a2 ≤ a1 and b1 ≤ b2. (Under the assumption a1 ≤ b1.)

Русский

Для любых a1 ≤ b1, выполняется Icc(a1,b1) ⊆ Icc(a2,b2) тогда и только если a2 ≤ a1 и b1 ≤ b2.

LaTeX

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

Lean4

theorem Icc_subset_Icc_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
  ⟨fun h => ⟨(h ⟨le_rfl, h₁⟩).1, (h ⟨h₁, le_rfl⟩).2⟩, fun ⟨h, h'⟩ _ ⟨hx, hx'⟩ => ⟨h.trans hx, hx'.trans h'⟩⟩

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