English
Given bases for two topologies, the induced infimum on a common domain has a natural basis described via preimages under the inducing maps.
Русский
Данные основы для двух топологий порождают ниспадающую сверху инфимную топологию на общем области, имеющую естественный базис через прообразы под маппингами.
LaTeX
$$$\\text{IsTopologicalBasis}(t := \\operatorname{induced} f_1 t \\sqcap \\operatorname{induced} f_2 s)(\\mathrm{image2}(f_1^{-1}'\\,\\cdot \\;\\cap\\; f_2^{-1}'\\,\\cdot)\\; B_1\\; B_2)$$$
Lean4
theorem inf_induced {γ} [s : TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁)
(h₂ : IsTopologicalBasis B₂) (f₁ : γ → α) (f₂ : γ → β) :
IsTopologicalBasis (t := induced f₁ t ⊓ induced f₂ s) (image2 (f₁ ⁻¹' · ∩ f₂ ⁻¹' ·) B₁ B₂) := by
simpa only [image2_image_left, image2_image_right] using (h₁.induced f₁).inf (h₂.induced f₂)
