of_isInducing — Mathlib

English

If B is a basis for open sets in β and f: α → β is inducing, then the pullback sets {f^{-1}(U) | U ∈ B} form a basis for opens in α.

Русский

Если B является базисом открытых множеств в β, а f: α → β индуцирует топологию, то перечень обратных изображений открытых U образует базис открытых множеств в α.

LaTeX

$$$\text{IsBasis}(B) \Rightarrow \text{IsBasis}({\langle f^{-1}(U), U.2.preimage f.continuous\rangle | U ∈ B})$$$

Lean4

theorem of_isInducing {B : Set (Opens β)} (H : IsBasis B) {f : α → β} (h : IsInducing f) :
    IsBasis ({⟨f ⁻¹' U, U.2.preimage h.continuous⟩ | U ∈ B}) :=
  by
  simp only [IsBasis] at H ⊢
  convert H.isInducing h
  ext; simp

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