snd_image_prod — Mathlib

English

If s is nonempty, then the second projection image of s × t equals t.

Русский

Если s непусто, то изображение второй координаты s × t равно t.

LaTeX

$$$ s.Nonempty \Rightarrow \mathrm{Prod.snd}'' (s \times t) = t $$$

Lean4

theorem snd_image_prod {s : Set α} (hs : s.Nonempty) (t : Set β) : Prod.snd '' s ×ˢ t = t :=
  (snd_image_prod_subset _ _).antisymm fun y y_in =>
    let ⟨x, x_in⟩ := hs
    ⟨(x, y), ⟨x_in, y_in⟩, rfl⟩

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