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⟩