Union_of_Transitive_Relations_Not_Always_Transitive
Provedproofwikirelation-theory
The union of transitive relations is not necessarily transitive.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Union_of_Transitive_Relations_Not_Always_Transitive : ∃ (R S : ℕ → ℕ → Prop), Transitive R ∧ Transitive S ∧ ¬Transitive (fun x y => R x y ∨ S x y) := by sorry
Source