coprod_neBot_iff — Mathlib

English

The coproduct of f and g is nonempty iff either f is nonempty and β is nonempty, or α is nonempty and g is nonempty.

Русский

Копродукт f и g не пуст тогда и только тогда, когда либо f непусто и β непусто, либо α непусто и g непусто.

LaTeX

$$$ (f.coprod g).NeBot \iff (f.NeBot \land \mathrm{Nonempty} \; \beta) \lor (\mathrm{Nonempty} \; \alpha \land g.NeBot) $$$

Lean4

theorem coprod_neBot_iff : (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot := by simp [Filter.coprod]

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