le_induced_generateFrom — Mathlib

English

If every a ∈ b has f^{-1}(a) open, then t ≤ induced f (generateFrom b).

Русский

Если для каждого a в b верно, что f^{-1}(a) открыто, то t ≤ индукцированная топология через f от generateFrom(b).

LaTeX

$$$(\forall a, a \in b \to IsOpen(f^{-1}' a)) \Rightarrow t \le \mathrm{induced}(f)(\mathrm{generateFrom}(b))$$$

Lean4

theorem le_induced_generateFrom {α β} [t : TopologicalSpace α] {b : Set (Set β)} {f : α → β}
    (h : ∀ a : Set β, a ∈ b → IsOpen (f ⁻¹' a)) : t ≤ induced f (generateFrom b) :=
  by
  rw [induced_generateFrom_eq]
  apply le_generateFrom
  simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp]
  exact h

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