English
Let α be a partially ordered set and s be a nonempty interval in α. Then the set of elements of α that lie in s is exactly s when viewed as a subset of α.
Русский
Пусть α — частично упорядоченное множество, и s — непустой интервал в α. Тогда множество элементов α, принадлежащих этому интервалу, совпадает с самим интервалом s при его рассмотрении как подмножества α.
LaTeX
$$$\\\\forall {\\\\alpha} [PartialOrder {\\\\alpha}] (s : NonemptyInterval {\\\\alpha}), \\\\big((s : Interval {\\\\alpha}) : Set {\\\\alpha}\\\\big) = s.$$$
Lean4
@[simp, norm_cast]
theorem coe_coe (s : NonemptyInterval α) : ((s : Interval α) : Set α) = s :=
rfl
