Union_of_Equivalences
Provedequivalence-relationsproofwikiset-unionunionunion-of-equivalences
The union of two equivalence relations is not necessarily an equivalence relation itself.
Preamble
import Mathlib.Data.Fin.Basic
Formal statement
theorem Union_of_Equivalences : ∃ (R₁ R₂ : Fin 3 → Fin 3 → Prop), (∀ x, R₁ x x) ∧ (∀ x y, R₁ x y → R₁ y x) ∧ (∀ x y z, R₁ x y → R₁ y z → R₁ x z) ∧ (∀ x, R₂ x x) ∧ (∀ x y, R₂ x y → R₂ y x) ∧ (∀ x y z, R₂ x y → R₂ y z → R₂ x z) ∧ ¬ (∀ x y z, (R₁ x y ∨ R₂ x y) → (R₁ y z ∨ R₂ y z) → (R₁ x z ∨ R₂ x z)) := by sorry
Source