Composite_Relation_with_Inverse_is_Symmetric
Provedproofwikisymmetric-relations
Let R ⊆ S × T be a relation. Then the composite R⁻¹ ∘ R is symmetric on S.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Composite_Relation_with_Inverse_is_Symmetric {α β : Type _} (R : α → β → Prop) (a b : α) (h : ∃ c, R a c ∧ R b c) : ∃ c, R b c ∧ R a c := by sorrySource