Icc_eq_singleton_iff — Mathlib

English

The closed interval [a,b] is a singleton {c} if and only if a = c and b = c.

Русский

Замкнутый интервал [a,b] является единственным множеством {c} тогда и только тогда, когда a = c и b = c.

LaTeX

$$$ Icc(a,b) = \{c\} \iff (a=c) \land (b=c).$$$

Lean4

@[simp]
theorem Icc_eq_singleton_iff : Icc a b = { c } ↔ a = c ∧ b = c :=
  by
  refine ⟨fun h => ?_, ?_⟩
  · have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
    exact ⟨eq_of_mem_singleton <| h ▸ left_mem_Icc.2 hab, eq_of_mem_singleton <| h ▸ right_mem_Icc.2 hab⟩
  · rintro ⟨rfl, rfl⟩
    exact Icc_self _

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