prod_neBot — Mathlib

English

NeBot (f × g) is equivalent to NeBot f and NeBot g: (f × g) is NeBot iff f and g are NeBot.

Русский

Неботовость произведения равна истине тогда, когда оба множителя неботовы: (f × g) NeBot ⇔ f.NeBot ∧ g.NeBot.

LaTeX

$$$ (f \\times\\! g) \\text{ is NeBot } \\iff (f \\text{ is NeBot}) \\wedge (g \\text{ is NeBot}) $$$

Lean4

theorem prod_neBot : NeBot (f ×ˢ g) ↔ NeBot f ∧ NeBot g := by simp only [neBot_iff, Ne, prod_eq_bot, not_or]

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