instSetLike — Mathlib

English

Opens α is equipped with a SetLike structure, i.e., opens can be identified with their underlying carriers as sets in α, and this identification is injective.

Русский

Открытые подмножества α образуют структуру SetLike, то есть можно однозначно идентифицировать открытое множество его карриером как множество в α.

LaTeX

$$$(\uparrow) : \mathrm{Opens}(\alpha) \to \mathcal{P}(\alpha)$ is injective, i.e., \forall U,V\in \mathrm{Opens}(\alpha), \uparrow U = \uparrow V \Rightarrow U = V.$$$

Lean4

instance : SetLike (Opens α) α where
  coe := Opens.carrier
  coe_injective' := fun ⟨_, _⟩ ⟨_, _⟩ _ => by congr

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