English
Let t be a topology on α and b a collection of subsets of β. A function f: α → β is continuous with respect to the generated topology generateFrom b if and only if for every s ∈ b, the preimage f^{-1}(s) is open.
Русский
Пусть t — топология на α, и b — семейство подмножеств β. Функция f: α → β непрерывна относительно порожденной топологии generateFrom b тогда и только тогда, когда для каждого s ∈ b множество f^{-1}(s) открыто.
LaTeX
$$$$ Continuous[t, \operatorname{generateFrom}(b)] f \iff \forall s \in b,\ IsOpen(f^{-1}(s)). $$$$
Lean4
theorem continuous_generateFrom_iff {t : TopologicalSpace α} {b : Set (Set β)} :
Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s) :=
by
rw [continuous_iff_coinduced_le, le_generateFrom_iff_subset_isOpen]
simp only [isOpen_coinduced, preimage_id', subset_def, mem_setOf]
