liftPropOn_of_liftProp — Mathlib

English

If a statement LiftProp P g holds, then the same propagates to LiftPropOn P g s for any s.

Русский

Если выполняется LiftProp P g, то аналогично выполняется LiftPropOn P g s для любого s.

LaTeX

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

Lean4

theorem liftPropOn_of_liftProp (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) (h : LiftProp P g) :
    LiftPropOn P g s := by
  rw [← liftPropOn_univ] at h
  exact liftPropOn_mono mono h (subset_univ _)

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