coinduced_le — Mathlib

English

There is a Galois connection between the coinduced and induced topologies along f: tα.coinduced f and tβ.induced f form a Galois connection.

Русский

Существует галуа-соотношение между коиндукцией и индукцией по отображению f: tα.coinduced f и tβ.induced f образуют галуа-соотношение.

LaTeX

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

Lean4

theorem coinduced_le (h : Continuous[t, t'] f) : t.coinduced f ≤ t' :=
  (@continuous_def α β t t').1 h

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