liftPropWithinAt_of_liftPropAt — Mathlib

English

If monotone condition holds for all s,t,f, then LiftPropWithinAt g s x is preserved under subset relations.

Русский

Если выполняется монотонное условие для всех s,t,f, LiftPropWithinAt сохраняется при вложении множеств.

LaTeX

$$(mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, s ⊆ t → P f s x → P f t x) → LiftPropWithinAt P g s x → s ⊆ t → LiftPropWithinAt P g t x$$

Lean4

theorem liftPropWithinAt_of_liftPropAt (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
    (h : LiftPropAt P g x) : LiftPropWithinAt P g s x :=
  by
  rw [← liftPropWithinAt_univ] at h
  exact liftPropWithinAt_mono mono h (subset_univ _)

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