gc_coinduced_induced — Mathlib

English

The same Galois connection between coinduced and induced topologies along f holds: coinduced ≤ induced correspondences.

Русский

Та же галуа-соотношение между коиндукцией и индукцией по f сохраняется.

LaTeX

$$$GaloisConnection(TopologicalSpace.coinduced f)(TopologicalSpace.induced f)$$$

Lean4

theorem gc_coinduced_induced (f : α → β) :
    GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f) := fun _ _ =>
  coinduced_le_iff_le_induced

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