productOfMemOpens_isInducing — Mathlib

English

The map productOfMemOpens is an inducing map from X into Opens(X) → Prop, i.e., X has the initial topology with respect to the family of evaluation maps x ↦ (x ∈ U).

Русский

Отображение productOfMemOpens является индуцирующим отображением X в Opens(X) → Prop, то есть топология X есть инициирующая относительно семейства отображений x ↦ (x ∈ U).

LaTeX

$$$\text{IsInducing}(\text{productOfMemOpens}(X)).$$$

Lean4

theorem productOfMemOpens_isInducing : IsInducing (productOfMemOpens X) :=
  by
  convert inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u
  apply eq_induced_by_maps_to_sierpinski

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