liftProp_of_locally_liftPropOn — Mathlib

English

Alternative formulation: if for every x there exists an open neighborhood giving LiftPropOn, then LiftPropOn on the whole set holds.

Русский

Альтернатива: если для каждой точки существует открытое множество, дающее LiftPropOn, то на всем множестве он выполняется.

LaTeX

$$$\mathrm{LiftPropOn\_iff} \; (\forall x\in M, \exists u,\text{IsOpen}(u) \land x\in u \land \mathrm{LiftPropOn}(P,g,s\cap u)).$$$

Lean4

theorem liftProp_of_locally_liftPropOn (h : ∀ x, ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u) : LiftProp P g :=
  by
  rw [← liftPropOn_univ]
  refine hG.liftPropOn_of_locally_liftPropOn fun x _ ↦ ?_
  simp [h x]

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