comap_id — Mathlib

English

The comap map of the identity continuous map is the identity on the opens lattice.

Русский

Комап по тождественному отображению равен тождественному отображению на множестве открытых множеств.

LaTeX

$$$\operatorname{comap}(\mathrm{ContinuousMap}.id\,\alpha) = \mathrm{FrameHom}.id(\operatorname{Opens}(\alpha))$$$

Lean4

@[simp]
theorem comap_id : comap (ContinuousMap.id α) = FrameHom.id _ :=
  FrameHom.ext fun _ => ext rfl

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