isTrans_inter — Mathlib

English

If R1 and R2 are transitive relations on α, then their intersection R1 ∩ R2 is transitive.

Русский

Если R1 и R2 — транзитивные отношения на α, то их пересечение R1 ∩ R2 тоже транзитивно.

LaTeX

$$$\forall a,b,c,\ (a,b) \in R_1 \cap R_2 \land (b,c) \in R_1 \cap R_2 \Rightarrow (a,c) \in R_1 \cap R_2$$$

Lean4

instance isTrans_inter [R₁.IsTrans] [R₂.IsTrans] : (R₁ ∩ R₂).IsTrans where
  trans _a _b _c hab hbc := ⟨R₁.trans hab.1 hbc.1, R₂.trans hab.2 hbc.2⟩

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