mono — Mathlib

English

If x is an accumulation point of F and F ≤ G, then x is an accumulation point of G.

Русский

Если x является точкой накопления фильтра F и F ≤ G, то x является точкой накопления фильтра G.

LaTeX

$$$AccPt\ x\ F \;\wedge\; F \le G \;\Longrightarrow\; AccPt\ x\ G$$

Lean4

/-- If `x` is an accumulation point of `F` and `F ≤ G`, then
`x` is an accumulation point of `G`. -/
theorem mono {F G : Filter X} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G :=
  NeBot.mono h (inf_le_inf_left _ hFG)

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