mem_inf_iff — Mathlib

English

For any f,g on α and s ⊆ α, s is in the infimum f ⊓ g if and only if there exists t1 ∈ f and t2 ∈ g with s = t1 ∩ t2.

Русский

Для любых фильтров f,g и множества s: s ∈ f ⊓ g тогда и только тогда, когда существуют t1 ∈ f и t2 ∈ g такие, что s = t1 ∩ t2.

LaTeX

$$$s \\in f \\sqcap g \\leftrightarrow \\exists t_1 \\in f, \\exists t_2 \\in g,\\ s = t_1 \\cap t_2$$$

Lean4

theorem mem_inf_iff {f g : Filter α} {s : Set α} : s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂ :=
  Iff.rfl

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