mem_pure — Mathlib

English

A set belongs to the principal ultrafilter at a if and only if a belongs to the set.

Русский

Множество принадлежит к главному ультрафильтру в точке a тогда и только тогда, когда a принадлежит этому множеству.

LaTeX

$$$ s \in (pure a : Ultrafilter \alpha) \iff a \in s $$$

Lean4

@[simp]
theorem mem_pure {a : α} {s : Set α} : s ∈ (pure a : Ultrafilter α) ↔ a ∈ s :=
  Iff.rfl

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