instCanLiftSetCoeIsClosed — Mathlib

English

If the underlying sets of two closed subsets coincide, then the closed subsets are equal.

Русский

Если основания двух замкнутых подмножеств совпадают, то сами множества совпадают.

LaTeX

$$$\forall s,t:\mathrm{Closeds}(\alpha),\ (s: \mathrm{Set} \alpha) = (t: \mathrm{Set} \alpha) \Rightarrow s = t$$$

Lean4

instance : CanLift (Set α) (Closeds α) (↑) IsClosed where prf s hs := ⟨⟨s, hs⟩, rfl⟩

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