liftPropOn_congr — Mathlib

English

Let G be LocalInvariantProp. Then LiftPropOn P g' s ↔ LiftPropOn P g s whenever g' y = g y for all y ∈ s.

Русский

Пусть G имеет локальную инвариантность. Тогда LiftPropOn P g' s эквивалентно LiftPropOn P g s, если g' совпадает с g на всех y ∈ s.

LaTeX

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

Lean4

theorem liftPropOn_congr (h : LiftPropOn P g s) (h₁ : ∀ y ∈ s, g' y = g y) : LiftPropOn P g' s := fun x hx ↦
  hG.liftPropWithinAt_congr (h x hx) h₁ (h₁ x hx)

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