image2 — Mathlib

English

The image2 f S T is nonempty if and only if S and T are nonempty: (image2 f S T).Nonempty ↔ S.Nonempty ∧ T.Nonempty.

Русский

Образ image2 f S T непуст тогда и только тогда, когда S и T непусты: (image2 f S T).Nonempty ⇔ S.Nonempty ∧ T.Nonempty.

LaTeX

$$$$\\bigl(\\operatorname{image2} f S T\\bigr) \\neq \\emptyset \\iff S \\neq \\emptyset \\land T \\neq \\emptyset.$$$$

Lean4

theorem image2 : s.Nonempty → t.Nonempty → (image2 f s t).Nonempty := fun ⟨_, ha⟩ ⟨_, hb⟩ =>
  ⟨_, mem_image2_of_mem ha hb⟩

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