English
If s is nonempty, the image of s under the universal relation on α is the universal set: image univ s = univ.
Русский
Если множество s непусто, образ от s при помощи всеобъемлющего отношения равен всеобщему множеству.
LaTeX
$$$\\forall (s : Set \\alpha), s.Nonempty \\rightarrow image Set.univ s = Set.univ$$$
Lean4
@[simp]
theorem image_univ_left (hs : s.Nonempty) : image (.univ : SetRel α β) s = .univ := by aesop