English
If a ≤ b, then Icc(a,b) = Icc(c,d) iff a = c and b = d.
Русский
Если a ≤ b, то Icc(a,b) = Icc(c,d) эквивалентно a = c и b = d.
LaTeX
$$$$ (a \\le b) \\Rightarrow (Icc(a,b) = Icc(c,d) \\iff a = c \\land b = d) $$$$
Lean4
theorem Icc_eq_Icc_iff {d : α} (h : a ≤ b) : Icc a b = Icc c d ↔ a = c ∧ b = d :=
by
refine ⟨fun heq ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
have h' : c ≤ d := by by_contra contra; rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq; contradiction
simp only [Set.ext_iff, mem_Icc] at heq
obtain ⟨-, h₁⟩ := (heq b).mp ⟨h, le_refl _⟩
obtain ⟨h₂, -⟩ := (heq a).mp ⟨le_refl _, h⟩
obtain ⟨h₃, -⟩ := (heq c).mpr ⟨le_refl _, h'⟩
obtain ⟨-, h₄⟩ := (heq d).mpr ⟨h', le_refl _⟩
exact ⟨le_antisymm h₃ h₂, le_antisymm h₁ h₄⟩
