mem_mul — Mathlib

English

For filters f and g and set s, s ∈ f * g iff ∃ t1 ∈ f, ∃ t2 ∈ g with t1 * t2 ⊆ s.

Русский

Для фильтров f и g и множества s верно: s ∈ f * g тогда и только тогда, когда существует t1 ∈ f и t2 ∈ g такие, что t1 * t2 ⊆ s.

LaTeX

$$$$ s \in f * g \iff \exists t_1 \in f, \exists t_2 \in g, t_1 * t_2 \subseteq s. $$$$

Lean4

@[to_additive]
theorem mem_mul : s ∈ f * g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ * t₂ ⊆ s :=
  Iff.rfl

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