sets_subset_sets

Mathlib.Order.Filter.Basic

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

English

For filters f,g on α, f.sets ⊆ g.sets if and only if g ≤ f in the filter order.

Русский

Для фильтров f,g на α выполнено f.sets ⊆ g.sets тогда и только тогда g ≤ f по порядку фильтров.

LaTeX

$$$f.sets \subseteq g.sets \iff g \le f$$$

Lean4

@[simp]
theorem sets_subset_sets : f.sets ⊆ g.sets ↔ g ≤ f :=
  .rfl

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

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

Разделы

Аффилиация

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