le_principal_iff

Mathlib.Order.Filter.Basic

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

English

For any set s and filter f, f ≤ 𝓟 s iff s ∈ f.

Русский

Для множества s и фильтра f верно: f ≤ 𝓟 s, если и только если s ∈ f.

LaTeX

$$$f \le 𝓟 s \iff s \in f$$$

Lean4

@[simp]
theorem le_principal_iff {s : Set α} {f : Filter α} : f ≤ 𝓟 s ↔ s ∈ f :=
  ⟨fun h => h Subset.rfl, fun hs _ ht => mem_of_superset hs ht⟩

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

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

Разделы

Аффилиация

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