instCanLiftSetCoeIsOpen — Mathlib

English

If U ≤ V for opens U,V, then the inclusion map from U to V is the natural inclusion sending x ∈ U to x ∈ V.

Русский

Если U ⊆ V для открытых U, V, то включение U в V есть естественное отображение x ∈ U ↦ x ∈ V.

LaTeX

$$$\forall U,V \in \mathrm{Opens}(\alpha),\; (U \le V) \Rightarrow \mathrm{inclusion}(U,V,h)(x)=x\quad (x\in U).$$$

Lean4

instance : CanLift (Set α) (Opens α) (↑) IsOpen :=
  ⟨fun s h => ⟨⟨s, h⟩, rfl⟩⟩

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