isTrans_univ — Mathlib

English

Let α be a type. The universal relation on α is transitive: for all a,b,c in α, if a is related to b and b is related to c under the universal relation, then a is related to c under the universal relation.

Русский

Пусть α — тип. Универсальное отношение на α транзитивно: для любых a,b,c ∈ α из-за того, что a связано c, и b связан c, следует, что a связан c.

LaTeX

$$$\forall a,b,c \in \alpha, (a,b) \in \mathrm{univ} \land (b,c) \in \mathrm{univ} \Rightarrow (a,c) \in \mathrm{univ}$$$

Lean4

instance isTrans_univ : SetRel.IsTrans (Set.univ : SetRel α α) where trans _ _ _ := by simp

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