liftPropWithinAt_mono — Mathlib

English

If a monotonicity relation holds between s and t and maps inside H to H', LiftPropWithinAt for g on t implies LiftPropWithinAt on s.

Русский

Если монотонность между s и t выполняется и отображения в H→H' соблюдают условие, то LiftPropWithinAt на t следует из LiftPropWithinAt на s.

LaTeX

$$(mono : ∀ {s x t}, s ⊆ t → P f s x → P f t x) → LiftPropWithinAt P g t → s ⊆ t → LiftPropWithinAt P g s$$

Lean4

theorem liftPropWithinAt_mono (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x) (h : LiftPropWithinAt P g s x)
    (hts : t ⊆ s) : LiftPropWithinAt P g t x :=
  by
  refine ⟨h.1.mono hts, mono (fun y hy ↦ ?_) h.2⟩
  simp only [mfld_simps] at hy
  simp only [hy, hts _, mfld_simps]

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