liftPropWithinAt_congr — Mathlib

English

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

Русский

Если LiftPropWithinAt P g s x выполняется и g' совпадает с g на 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 (h : LiftPropWithinAt P g s x) (h₁ : ∀ y ∈ s, g' y = g y) (hx : g' x = g x) :
    LiftPropWithinAt P g' s x :=
  (hG.liftPropWithinAt_congr_iff h₁ hx).mpr h

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