English
The topology on α induced by f from generateFrom b is equal to the topology generated by preimages of b under f.
Русский
Топология на α, индуцированная через f от generateFrom b, равна топологии, генерируемой обратными образами множества b.
LaTeX
$$$ (\mathrm{generateFrom}(b)).induced f = \mathrm{generateFrom}(\mathrm{preimage} f '' b)$$$
Lean4
theorem induced_generateFrom_eq {α β} {b : Set (Set β)} {f : α → β} :
(generateFrom b).induced f = generateFrom (preimage f '' b) :=
le_antisymm (le_generateFrom <| forall_mem_image.2 fun s hs => ⟨s, GenerateOpen.basic _ hs, rfl⟩)
(coinduced_le_iff_le_induced.1 <| le_generateFrom fun _s hs => .basic _ (mem_image_of_mem _ hs))
