preimage_subset_source — Mathlib

English

If s is a subset of the base set of the trivialization, then the preimage proj^{-1}(s) lies inside the domain of the trivialization (the source).

Русский

Если s ⊆ baseSet тривиализации, то предобраз proj^{-1}(s) ⊆ source тривиализации.

LaTeX

$$$ s \subseteq e.baseSet \Rightarrow proj^{-1}(s) \subseteq e.source $$$

Lean4

theorem preimage_subset_source {s : Set B} (hb : s ⊆ e.baseSet) : proj ⁻¹' s ⊆ e.source := fun _p hp =>
  e.mem_source.mpr (hb hp)

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