liftPropOn_mono — Mathlib

English

If a monotone property holds for all contained sets, then LiftPropOn is monotone with respect to inclusion of sets.

Русский

Если монотонное свойство держится для всех вложенных множеств, то LiftPropOn монотонно по включению множеств.

LaTeX

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

Lean4

theorem liftPropOn_mono (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) (h : LiftPropOn P g t)
    (hst : s ⊆ t) : LiftPropOn P g s := fun x hx ↦ liftPropWithinAt_mono mono (h x (hst hx)) hst

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