join_mono

Mathlib.Order.Filter.Basic

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

English

The join operation on filters is monotone: if f1 ≤ f2 then join(f1) ≤ join(f2).

Русский

Операция объединения фильтров монотонна: если f1 ≤ f2, то join(f1) ≤ join(f2).

LaTeX

$$$f_1 \\le f_2 \\Rightarrow join(f_1) \\le join(f_2)$$$

Lean4

@[mono, gcongr]
theorem join_mono {f₁ f₂ : Filter (Filter α)} (h : f₁ ≤ f₂) : join f₁ ≤ join f₂ := fun _ hs => h hs

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

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

Разделы

Аффилиация

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