preimage_univ_left — Mathlib

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

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