opensRange_pullback_snd_of_left — Mathlib

English

In the same setting, the opensRange of pullback.snd g f coincides with the preimage under map (Opens.map) g.base of the opensRange of f; equivalently, the open set associated to pullback via fst equals the preimage of f.opensRange along g.

Русский

В той же ситуации открытое множество, соответствующее pullback.snd, совпадает с предобразом по g.base открытого множества f.opensRange, то есть opensRange pullback совпадает с g^{-1}(f.opensRange).

LaTeX

$$$\\text{pullback.openRange.pullback_fst_of_right} \\quad : \\ (pullback.fst\\ g\\ f).base = ((Opens.map g.base).obj ⟨Set.range f.base, \\text{isOpen_range}⟩).1$$$

Lean4

theorem opensRange_pullback_snd_of_left : (pullback.snd f g).opensRange = g ⁻¹ᵁ f.opensRange :=
  Opens.ext (range_pullback_snd_of_left f g)

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