WithUpperSetHomeomorph — Mathlib

English

If α has an upper-set topology, then WithUpperSet α is homeomorphic to α via a canonical isomorphism.

Русский

Если у α есть верхнетопологическое устройство, то WithUpperSet α гомоморфно эквивалентно α посредством канонического отображения.

LaTeX

$$$ \mathrm{WithUpperSet}(\alpha) \simeq_t \alpha. $$$

Lean4

/-- If `α` is equipped with the upper set topology, then it is homeomorphic to
`WithUpperSet α`. -/
def WithUpperSetHomeomorph : WithUpperSet α ≃ₜ α :=
  WithUpperSet.ofUpperSet.toHomeomorphOfIsInducing ⟨topology_eq α ▸ induced_id.symm⟩

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