Ioc_subset_Ioc_iff — Mathlib

English

For a1 < b1, the half-open interval Ioc(a1, b1) ⊆ Ioc(a2, b2) holds exactly when b1 ≤ b2 and a2 ≤ a1.

Русский

Для a1 < b1 включение Ioc(a1, b1) ⊆ Ioc(a2, b2) эквивалентно b1 ≤ b2 и a2 ≤ a1.

LaTeX

$$$ a_1 < b_1 \Rightarrow \left( (a_1, b_1] \subseteq (a_2, b_2] \iff b_1 \le b_2 \land a_2 \le a_1 \right)$$$

Lean4

theorem Ioc_subset_Ioc_iff (h₁ : a₁ < b₁) : Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁ := by
  convert @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2 <;> exact (@Ico_toDual α _ _ _).symm

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