mono — Mathlib

English

Inclusion s' ⊆ s propagates to UniformCauchySeqOn via mono_left or mono_right.

Русский

Включение подмножества переносится к UniformCauchySeqOn через mono_left/mono_right.

LaTeX

$$$UniformCauchySeqOn F p s \to s' \subseteq s \\Rightarrow UniformCauchySeqOn F p s'$$$

Lean4

theorem mono (hf : UniformCauchySeqOn F p s) (hss' : s' ⊆ s) : UniformCauchySeqOn F p s' :=
  by
  rw [uniformCauchySeqOn_iff_uniformCauchySeqOnFilter] at hf ⊢
  exact hf.mono_right (le_principal_iff.mpr <| mem_principal.mpr hss')

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