image2_eq_empty_iff — Mathlib

English

image2 f S T is empty if and only if S is empty or T is empty: image2 f S T = ∅ ⇔ S = ∅ ∨ T = ∅.

Русский

image2 f S T пусто тогда и только тогда, когда S пусто или T пусто.

LaTeX

$$$$ \\operatorname{image2} f S T = \\emptyset \\iff S = \\emptyset \\lor T = \\emptyset. $$$$

Lean4

@[simp]
theorem image2_eq_empty_iff : image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅ :=
  by
  rw [← not_nonempty_iff_eq_empty, image2_nonempty_iff, not_and_or]
  simp [not_nonempty_iff_eq_empty]

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