Grace/Cumulus/Relation/Core.g17

Open in Workbench Download source

Imports

Algebra.Foundation

Declarations

• RelationOn predicate
• IrreflexiveOn predicate
• SymmetricOn predicate
• ConnectedOn predicate
• Equivalence predicate
• RelationBetween.bounds theorem derivation
• converse def
• converse.relates theorem derivation
• converse.reflects theorem derivation
• converse.relation theorem derivation
• converse.bounds theorem derivation
• Equivalence.relation theorem derivation
• Equivalence.reflexive theorem derivation
• Equivalence.symmetric theorem derivation
• Equivalence.transitive theorem derivation

Source

1-- Relations and equivalence relations2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Relation.Core8import Algebra.Foundation910predicate RelationOn (r A : Set) := RelationBetween(r, A, A)11predicate IrreflexiveOn (A r : Set) := ∀ x ∈ A, ¬relates(r, x, x)12predicate SymmetricOn (A r : Set) := ∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(r, y, x)13predicate ConnectedOn (A r : Set) := ∀ x ∈ A, ∀ y ∈ A, x ≠ y → (relates(r, x, y) ∨ relates(r, y, x))14predicate Equivalence (A r : Set) := RelationOn(r, A) ∧ (ReflexiveOn(A, r) ∧ (SymmetricOn(A, r) ∧ TransitiveOn(A, r)))1516theorem RelationBetween.bounds (r A B x y : Set)17  requires relation : RelationBetween(r, A, B)18  requires hxy : relates(r, x, y)19  shows x ∈ A ∧ y ∈ B20proof21  unfold RelationBetween at relation22  specialize relation with (x, y), hxy23  obtain ⟨bounded, a, haA, b, hbB, pairShape⟩ := product.membership.forward with relation24  obtain (xEquals, yEquals) := orderedPair.injective with pairShape25  rw [xEquals, yEquals]26  refine ⟨haA, hbB⟩2728-- Converse is bounded by the reversed Cartesian product, so it is a set.29def converse (r A B : Set) : Set := { p ∈ B × A | ∃ x ∈ A, ∃ y ∈ B, p = (y, x) ∧ relates(r, x, y) }3031theorem converse.relates (r A B x y : Set)32  requires hx : x ∈ A33  requires hy : y ∈ B34  requires hxy : relates(r, x, y)35  shows relates(converse(r, A, B), y, x)36proof37  simp [relates, converse.membership, product.pair]3839theorem converse.reflects (r A B x y : Set)40  requires hxy : relates(converse(r, A, B), y, x)41  shows relates(r, x, y)42proof43  unfold relates at hxy44  simp [converse.membership] at hxy45  rcases hxy with ⟨hProduct, a, haA, b, hbB, hPair, hab⟩46  obtain ⟨hyb, hxa⟩ := orderedPair.injective with hPair47  rw ← hxa at hab48  rwa ← hyb at hab4950theorem converse.relation (r A B : Set)51  shows RelationBetween(converse(r, A, B), B, A)52proof53  simp [RelationBetween, Subset]5455theorem converse.bounds (r A B x y : Set)56  requires hxy : relates(converse(r, A, B), y, x)57  shows y ∈ B ∧ x ∈ A58proof59  unfold relates at hxy60  simp [converse.membership] at hxy61  rcases hxy with ⟨hProduct, a, haA, b, hbB, hPair, hab⟩62  obtain ⟨hyb, hxa⟩ := orderedPair.injective with hPair63  constructor64  rwa hyb65  rwa hxa6667theorem Equivalence.relation (A r : Set)68  requires h : Equivalence(A, r)69  shows RelationOn(r, A)70proof71  rcases h with ⟨relation, laws⟩72  exact relation7374theorem Equivalence.reflexive (A r : Set)75  requires h : Equivalence(A, r)76  shows ReflexiveOn(A, r)77proof78  simp [Equivalence]7980theorem Equivalence.symmetric (A r : Set)81  requires h : Equivalence(A, r)82  shows SymmetricOn(A, r)83proof84  simp [Equivalence]8586theorem Equivalence.transitive (A r : Set)87  requires h : Equivalence(A, r)88  shows TransitiveOn(A, r)89proof90  simp [Equivalence]91