coe_eq_pure — Mathlib

English

Equality of the lifted nonempty interval to a pure interval is equivalent to equality of the underlying nonempty interval to the pure nonempty interval.

Русский

Равенство возведённого в Some интервала равному чистому интервалу эквивалентно равенству базового некогда пустого интервала чистому интервалу.

LaTeX

$$$$ (WithBot.some s) = (Interval.pure a) \\;\\iff\\; s = pure a. $$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_pure : (s : Interval α) = Interval.pure a ↔ s = pure a := by rw [← Interval.coe_inj, coe_pure_interval]

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