mono — Mathlib

English

The operation ContinuousOn is antitone with respect to inclusion: if t ⊆ s and f is continuous on s, then f is continuous on t.

Русский

Операция ContinuousOn антимонотна по включению: если t ⊆ s и f непрерывна на s, то она непрерывна на t.

LaTeX

$$$$\text{ContinuousOn}(f,t)\quad\text{whenever}\quad \text{ContinuousOn}(f,s) \text{ and } t \subseteq s.$$$$

Lean4

theorem mono (hf : ContinuousOn f s) (h : t ⊆ s) : ContinuousOn f t := fun x hx =>
  (hf x (h hx)).mono_left (nhdsWithin_mono _ h)

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