principal_singleton

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.principal_singleton

English

The principal filter of a singleton equals the pure image at that point: 𝓟{a} = pure a.

Русский

Принципиальный фильтр пары тождественен: 𝓟{a} = pure a.

LaTeX

$$principal_singleton (a) : 𝓟 { a } = pure a$$

Lean4

@[simp]
theorem principal_singleton (a : α) : 𝓟 { a } = pure a :=
  Filter.ext fun s => by simp only [mem_pure, mem_principal, singleton_subset_iff]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru