join_pure

Mathlib.Order.Filter.Map

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

English

The join of a pure filter equals the filter itself: join (pure f) = f.

Русский

Объединение чистого фильтра равно самому фильтру: join (pure f) = f.

LaTeX

$$join_pure (f : Filter α) : join (pure f) = f$$

Lean4

@[simp]
theorem join_pure (f : Filter α) : join (pure f) = f :=
  rfl

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

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

Разделы

Аффилиация

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