principal_bind — Mathlib

English

The bind of a principal filter equals the supremum of the family: bind (𝓟 s) f = ⨆ x ∈ s, f x.

Русский

Связывание принципиального фильтра равно супремуму семейства: bind (𝓟 s) f = ⨆ x ∈ s, f x.

LaTeX

$$$\\mathrm{bind}(\\mathcal{P} s)\\ f = \\bigvee_{x \\in s} f(x)$$$

Lean4

theorem principal_bind {s : Set α} {f : α → Filter β} : bind (𝓟 s) f = ⨆ x ∈ s, f x :=
  show join (map f (𝓟 s)) = ⨆ x ∈ s, f x by simp only [sSup_image, join_principal_eq_sSup, map_principal]

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