liftPropWithinAt_mono_of_mem_nhdsWithin

English

If a monotonicity condition holds for P with respect to containment of domains, then LiftPropWithinAt is preserved when moving from s to t with s ∈ 𝓝[t] x.

Русский

Если выполнено монотонностное условие для P по включению областей, то LiftPropWithinAt сохраняется при переходе от s к t при условии s ∈ 𝓝[t] x.

LaTeX

$$$(mono\_of\_mem\_nhdsWithin)\; (h : LiftPropWithinAt P g s x)\; (hst : s ∈ 𝓝[t] x)\;\to\; LiftPropWithinAt P g t x$$

Lean4

theorem liftPropWithinAt_mono_of_mem_nhdsWithin
    (mono_of_mem_nhdsWithin : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x) (h : LiftPropWithinAt P g s x)
    (hst : s ∈ 𝓝[t] x) : LiftPropWithinAt P g t x :=
  by
  simp only [liftPropWithinAt_iff'] at h ⊢
  refine ⟨h.1.mono_of_mem_nhdsWithin hst, mono_of_mem_nhdsWithin ?_ h.2⟩
  simp_rw [← mem_map, (chartAt H x).symm.map_nhdsWithin_preimage_eq (mem_chart_target H x),
    (chartAt H x).left_inv (mem_chart_source H x), hst]

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