liftPropWithinAt_self — Mathlib

English

For germs in a model space H, LiftPropWithinAt P f s x is equivalent to ContinuousWithinAt f s x and P f s x.

Русский

Для каска f в модели H, LiftPropWithinAt P f s x равно ContinuousWithinAt f s x ∧ P f s x.

LaTeX

$$$\mathrm{LiftPropWithinAt}(P,f,s,x) \iff \big( \mathrm{ContinuousWithinAt}(f,s,x) \wedge P(f,s,x)\big).$$$

Lean4

theorem liftPropWithinAt_self {f : H → H'} {s : Set H} {x : H} :
    LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P f s x :=
  liftPropWithinAt_iff' ..

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