eq_pure_of_finite — Mathlib

English

Same content as above: if a finite set is in an ultrafilter, the ultrafilter is principal at some element of the set.

Русский

То же самое: если конечный набор принадлежит ультрафильтру, он равен чистому ультрафильтру по некоторому элементу набора.

LaTeX

$$$s\text{ finite} \land s \in f \Rightarrow \exists x\in s,\ f = \mathrm{pure}\, x$$

Lean4

theorem eq_pure_of_finite [Finite α] (f : Ultrafilter α) : ∃ a, f = pure a :=
  (eq_pure_of_finite_mem finite_univ univ_mem).imp fun _ ⟨_, ha⟩ => ha

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