principal_eq_iff_eq

Mathlib.Order.Filter.Basic

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

English

Two principal filters are equal iff their generating sets are equal.

Русский

Два порождающих фильтра равны тогда и только тогда, когда их порождающие множества равны.

LaTeX

$$$𝓟 s = 𝓟 t \iff s = t$$$

Lean4

@[simp]
theorem principal_eq_iff_eq {s t : Set α} : 𝓟 s = 𝓟 t ↔ s = t := by
  simp only [le_antisymm_iff, le_principal_iff, mem_principal]; rfl

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

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

Разделы

Аффилиация

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