English
If t is nonempty, then the two-argument image2 with the first projection equal to the identity on the first coordinate and the second coordinate varying over t collapses to s; more concretely, image2 (λ x _ => x) s t = s when t is nonempty.
Русский
Если множество t непусто, то образ2 (λ x _ => x) над s и t совпадает с s; то есть image2 (λ x _ => x) s t = s при t ≠ пустое.
LaTeX
$$$\\text{If } t \\neq \\varnothing,\\quad \\operatorname{image}_2(\\lambda x\\,\\_ . x)\\, s\\, t = s$$$
Lean4
@[simp]
theorem image2_left (h : t.Nonempty) : image2 (fun x _ => x) s t = s := by simp [nonempty_def.mp h, Set.ext_iff]
