univ_comp — Mathlib

English

Similarly, composing the universal relation on α to β with S yields all pairs where the second coordinate lies in the codomain of S: Univ ○ S = { (a,c) ∈ α × γ | c ∈ cod(S) }.

Русский

Аналогично, композиция всеобъемлющего отношения слева с S даёт пары (a,c) такие что c принадлежит cod(S).

LaTeX

$$$\mathrm{univ} \circ S = \{(a,c) \in \alpha \times \gamma \mid c \in \mathrm{cod}(S)\}$$$

Lean4

@[simp]
theorem univ_comp (S : SetRel β γ) : (.univ : SetRel α β) ○ S = {(_b, c) : α × γ | c ∈ S.cod} := by aesop

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