mul_neBot_iff — Mathlib

English

The product f * g is nontrivial if and only if both f and g are nontrivial.

Русский

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

LaTeX

$$$$ (f * g).NeBot \iff f.NeBot \land g.NeBot. $$$$

Lean4

@[to_additive (attr := simp)] -- TODO: make this a scoped instance in the `Pointwise` namespace

theorem mul_neBot_iff : (f * g).NeBot ↔ f.NeBot ∧ g.NeBot :=
  map₂_neBot_iff

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