image2_nonempty_iff — Mathlib

English

Variant of the nonemptiness criterion: (image2 f S T).Nonempty ↔ S.Nonempty ∧ T.Nonempty (simp variant).

Русский

Вариант критерия непустоты: (image2 f S T).Nonempty ⇔ S.Nonempty ∧ T.Nonempty (вариант, помеченный simp).

LaTeX

$$$$\\operatorname{image2} f S T \\text{ is nonempty } \\iff S \\text{ and } T \\text{ are nonempty}.$$$$

Lean4

@[simp]
theorem image2_nonempty_iff : (image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  ⟨fun ⟨_, a, ha, b, hb, _⟩ => ⟨⟨a, ha⟩, b, hb⟩, fun h => h.1.image2 h.2⟩

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