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