div_bot

Mathlib.Order.Filter.Pointwise

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

English

Dividing by the bottom filter yields bottom: f / ⊥ = ⊥.

Русский

Деление на нижний фильтр даёт нижний фильтр: f / ⊥ = ⊥.

LaTeX

$$$f / \\perp = \\perp.$$$

Lean4

@[to_additive (attr := simp)]
theorem div_bot : f / ⊥ = ⊥ :=
  map₂_bot_right

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

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

Разделы

Аффилиация

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