smul_eq_bot_iff — Mathlib

English

Let f be a filter on α and g a filter on β with a compatible scalar action of α on β. The product filter f • g equals the bottom filter if and only if either f = ⊥ or g = ⊥.

Русский

Пусть f — фильтр на α и g — фильтр на β, при наличии совместного действия α на β. Произведение фильтров f • g равно ⊥ тогда и только тогда, когда либо f = ⊥, либо g = ⊥.

LaTeX

$$$ f \cdot g = \bot \iff f = \bot \lor g = \bot $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_eq_bot_iff : f • g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
  map₂_eq_bot_iff

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