Icc_subset_Ioo_iff — Mathlib

English

For a1 ≤ b1, the closed interval [a1,b1] is contained in the open interval (a2,b2) iff a2 < a1 and b1 < b2.

Русский

При a1 ≤ b1 множество [a1,b1] содержится в (a2,b2) тогда и только если a2 < a1 и b1 < b2.

LaTeX

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

Lean4

theorem Icc_subset_Ioo_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioo 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_le hx, hx'.trans_lt h'⟩⟩

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