mem_sup — Mathlib

English

For any filters f and g on α and any subset s ⊆ α, membership in the join is exactly the conjunction of membership in f and membership in g: s ∈ f ⊔ g iff s ∈ f and s ∈ g.

Русский

Для фильтров f и g на α и множества s ⊆ α верно: s ∈ f ⊔ g тогда и только тогда, когда s ∈ f и s ∈ g.

LaTeX

$$$s \in f \sqcup g \;\iff\; (s \in f) \land (s \in g)$$$

Lean4

@[simp]
theorem mem_sup {f g : Filter α} {s : Set α} : s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g :=
  Iff.rfl

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