image_univ_left — Mathlib

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

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