mono'

Mathlib.Topology.UniformSpace.Cauchy

URI: https://scilib.ai/kg/mathlib#Cauchy.mono'

English

A variant stating monotonicity of Cauchy with a nontrivial filter g below f.

Русский

variant говорит о монотонности Коши при неотрезаном фильтре g ниже f.

LaTeX

$$$ Cauchy(f) \rightarrow NeBot(g) \rightarrow g \le f \rightarrow Cauchy(g) $$$

Lean4

theorem mono' {f g : Filter α} (h_c : Cauchy f) (_ : NeBot g) (h_le : g ≤ f) : Cauchy g :=
  h_c.mono h_le

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru