comp_univ — Mathlib

English

For a relation R: SetRel α β, composing with the universal relation on β to γ yields all pairs whose first coordinate lies in the domain of R: R ○ Univ = { (a,c) ∈ α × γ | a ∈ dom(R) }.

Русский

Для отношения R: SetRel α β композиция с всеобъемлющим отношением на β→γ даёт все пары с первой координатой a из dom(R): R ○ Univ = { (a,c) ∈ α × γ | a ∈ dom(R) }.

LaTeX

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

Lean4

@[simp]
theorem comp_univ (R : SetRel α β) : R ○ (.univ : SetRel β γ) = {(a, _c) : α × γ | a ∈ R.dom} := by aesop

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