coe_fst_eventuallyEq_proj' — Mathlib

English

If x lies in the base set of the trivialization e, then near x the first coordinate of e agrees with the base projection proj; i.e., the two maps coincide on a neighborhood of x in the nhds filter.

Русский

Если x принадлежит базовому множеству тривиализации e, то в окрестности x первая координата трактивизации совпадает с отображением proj.

LaTeX

$$$ (Prod.fst \circ e) =^{\mathcal{N} x} proj $$$

Lean4

theorem coe_fst_eventuallyEq_proj' (ex : proj x ∈ e.baseSet) : Prod.fst ∘ e =ᶠ[𝓝 x] proj :=
  e.coe_fst_eventuallyEq_proj (e.mem_source.2 ex)

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