antitone_continuousOn — Mathlib

English

The map s ↦ ContinuousOn f s is antitone: if s ⊆ t, then ContinuousOn f t ⇒ ContinuousOn f s.

Русский

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

LaTeX

$$$$\forall s,t,\; t \subseteq s \Rightarrow (\text{ContinuousOn}(f,s) \Rightarrow \text{ContinuousOn}(f,t)).$$$$

Lean4

theorem antitone_continuousOn {f : α → β} : Antitone (ContinuousOn f) := fun _s _t hst hf => hf.mono hst

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