eq_pure_iff

Mathlib.Order.Filter.Ultrafilter.Defs

URI: https://scilib.ai/kg/mathlib#Filter.NeBot.eq_pure_iff

English

If f is nonempty, then f = pure x iff {x} ∈ f.

Русский

Если f ненулевой, то f = pure x тогда и только тогда, когда {x} ∈ f.

LaTeX

$$$ f.NeBot \to (f = pure x \iff {x} \in f) $$$

Lean4

protected theorem eq_pure_iff (hf : f.NeBot) {x : α} : f = pure x ↔ { x } ∈ f := by rw [← hf.le_pure_iff, le_pure_iff]

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

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

Разделы

Аффилиация

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