Ico_eq_Ico_iff — Mathlib

English

If at least one of the half-open intervals Ico(a1, b1) or Ico(a2, b2) is nonempty (a1 < b1 or a2 < b2), then equality Ico(a1, b1) = Ico(a2, b2) is equivalent to a1 = a2 and b1 = b2.

Русский

Если хотя бы один из полузакрытых интервалов Ico(a1, b1) или Ico(a2, b2) непуст, то равенство Ico(a1, b1) = Ico(a2, b2) эквивалентно a1 = a2 и b1 = b2.

LaTeX

$$$ (a_1 < b_1) \lor (a_2 < b_2) \Rightarrow \left( Ico(a_1,b_1) = Ico(a_2,b_2) \iff a_1 = a_2 \land b_1 = b_2 \right)$$$

Lean4

theorem Ico_eq_Ico_iff (h : a₁ < b₁ ∨ a₂ < b₂) : Ico a₁ b₁ = Ico a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ :=
  ⟨fun e => by
    simp only [Subset.antisymm_iff] at e
    simp only [le_antisymm_iff]
    rcases h with h | h <;> simp only [Ico_subset_Ico_iff h] at e <;> [rcases e with ⟨⟨h₁, h₂⟩, e'⟩;
          rcases e with ⟨e', ⟨h₁, h₂⟩⟩] <;>
        have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e' <;>
      tauto,
    fun ⟨h₁, h₂⟩ => by rw [h₁, h₂]⟩

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