Icc_subset_Ioc_iff — Mathlib

English

If a1 ≤ b1, then Icc(a1,b1) ⊆ Ioc(a2,b2) is equivalent to a2 < a1 and b1 ≤ b2.

Русский

Если a1 ≤ b1, то Icc(a1,b1) ⊆ Ioc(a2,b2) эквивалентно a2 < a1 и b1 ≤ b2.

LaTeX

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

Lean4

theorem Icc_subset_Ioc_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂ :=
  (Icc_subset_Ico_iff h₁.dual).trans and_comm

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