mem_join — Mathlib

English

The membership criterion for join is stable under a straightforward equivalence; s ∈ join f iff the corresponding set membership is equivalent to membership in f.

Русский

Критерий принадлежности для join сводится к простой эквивалентности между членством множества и членством фильтра f.

LaTeX

$$$ s \in join f \iff s \in setOf(\dots) . $$$

Lean4

@[simp]
theorem mem_join {s : Set α} {f : Filter (Filter α)} : s ∈ join f ↔ {t | s ∈ t} ∈ f :=
  Iff.rfl

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