smul_neBot_iff — Mathlib

English

Let f and g be filters on α and β, respectively. Then the product filter f • g is nontrivial if and only if both f and g are nontrivial.

Русский

Пусть f и g — фильтры на α и β соответственно. Тогда произведение f • g не тривиально тогда, когда оба фактора не тривиальны.

LaTeX

$$$ (f \cdot g).\mathrm{NeBot} \iff f.\mathrm{NeBot} \land g.\mathrm{NeBot} $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_neBot_iff : (f • g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff

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