generate_singleton — Mathlib

English

Let s be a subset of α. Then the filter generated by the singleton {s} equals the principal filter on s.

Русский

Пусть s ⊆ α. Тогда фильтр, порожденный одиночным множеством {s}, равен примитивному фильтру на s.

LaTeX

$$$\\operatorname{generate}(\\{s\\}) = \\mathcal{P}(s)$$$

Lean4

@[simp]
theorem generate_singleton (s : Set α) : generate { s } = 𝓟 s :=
  le_antisymm (fun _t ht ↦ mem_of_superset (mem_generate_of_mem <| mem_singleton _) ht) <|
    le_generate_iff.2 <| singleton_subset_iff.2 Subset.rfl

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