of_inf_right — Mathlib

English

The map-cluster-point predicate satisfies that MapClusterPt x F u is equivalent to ClusterPt x (map u F).

Русский

Утверждение о сопоставлении кластерной точки сохраняется: MapClusterPt x F u эквивалентно ClusterPt x (map u F).

LaTeX

$$$\\mathrm{MapClusterPt}(x,F,u) \\iff \\mathrm{ClusterPt}(x,\\mathrm{map}\\;u\\;F)$$$

Lean4

theorem of_inf_right {f g : Filter X} (H : ClusterPt x <| f ⊓ g) : ClusterPt x g :=
  H.mono inf_le_right

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