comap_comp — Mathlib

English

If β is T0, the comap map is injective on opens.

Русский

Если β удовлетворяет свойству T0, отображение comap на множестве открытых множеств инъективно.

LaTeX

$$$[T0Space\ β] \Rightarrow Injective\ (comap : C(\alpha, \beta) \to FrameHom(Opens(\beta), Opens(\alpha)))$$$

Lean4

protected theorem comap_comp (g : C(β, γ)) (f : C(α, β)) : comap (g.comp f) = (comap f).comp (comap g) :=
  rfl

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