specializes_iff_le

Mathlib.Topology.Filter

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

← MathLib Explorer

English

l1 specializes l2 if and only if l1 ≤ l2.

Русский

l1 специализируется на l2 тогда же, когда l1 ≤ l2.

LaTeX

$$$l_1 \;\mathrel{\rhd}\; l_2 \quad\iff\quad l_1 \le l_2.$$$

Lean4

@[simp]
theorem specializes_iff_le {l₁ l₂ : Filter α} : l₁ ⤳ l₂ ↔ l₁ ≤ l₂ := by
  simp only [specializes_iff_closure_subset, Filter.closure_singleton, Ici_subset_Ici]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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