English
Given f: X → Y and a topology on X, the coinduced topology on Y is the finest topology making f continuous; a set s is open in Y iff f⁻¹(s) is open in X.
Русский
Дана функция f: X → Y и топология на X; коиндуцированная топология на Y — наиболее точная топология, делающая f непрерывной; множество s открыто в Y тогда и только тогда, когда его прообраз открыт в X.
LaTeX
$$def coinduced (f : X → Y) (t : TopologicalSpace X) : TopologicalSpace Y :=$$
Lean4
/-- Given `f : X → Y` and a topology on `X`,
the coinduced topology on `Y` is defined such that
`s : Set Y` is open if the preimage of `s` is open.
This is the finest topology that makes `f` continuous. -/
def coinduced (f : X → Y) (t : TopologicalSpace X) : TopologicalSpace Y
where
IsOpen s := IsOpen (f ⁻¹' s)
isOpen_univ := t.isOpen_univ
isOpen_inter _ _ h₁ h₂ := h₁.inter h₂
isOpen_sUnion s h := by simpa only [preimage_sUnion] using isOpen_biUnion h
