continuousWithinAt — Mathlib

English

For any p and any set s, the map x ↦ p.eval x is continuous within s at any point a.

Русский

Для любого p и любого множества s отображение x ↦ p.eval x непрерывно внутри s в точке a.

LaTeX

$$$\\forall p, s, a,\\; ContinuousWithinAt(\\lambda x. p.eval x, s, a)$$$

Lean4

@[fun_prop]
protected theorem continuousWithinAt {s a} : ContinuousWithinAt (fun x => p.eval x) s a :=
  p.continuous.continuousWithinAt

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