liftPropWithinAt_congr_of_mem — Mathlib

English

If LiftPropWithinAt P g s x holds, and g' agrees with g on s and x ∈ s, then LiftPropWithinAt P g' s x.

Русский

Если LiftPropWithinAt P g s x выполняется и g' совпадает с g на s, и x ∈ s, тогда LiftPropWithinAt P g' s x.

LaTeX

$$$G.LocalInvariantProp\ G' P \to\ LiftPropWithinAt\ P\ g\ s\ x \to\ (\forall y \in s, g' y = g y) \to x \in s \to LiftPropWithinAt\ P\ g'\ s\ x$$

Lean4

theorem liftPropWithinAt_congr_of_mem (h : LiftPropWithinAt P g s x) (h₁ : ∀ y ∈ s, g' y = g y) (hx : x ∈ s) :
    LiftPropWithinAt P g' s x :=
  (hG.liftPropWithinAt_congr_iff h₁ (h₁ _ hx)).mpr h

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