Grace/Cumulus/Relation/Quotient.g17

Open in Workbench Download source

Imports

Relation · Set

Declarations

• equivalenceClass def
• quotient def
• equivalenceClass.subset theorem derivation
• equivalenceClass.self theorem derivation
• equivalenceClass.eq theorem derivation
• equivalenceClass.members_related theorem derivation
• equivalenceClass.related_of_eq theorem derivation
• quotient.contains_class theorem derivation
• quotient.subset_powerset theorem derivation
• quotient.member_nonempty theorem derivation
• quotient.members_related theorem derivation
• quotient.class_of_member theorem derivation

Source

1-- Equivalence classes and quotient sets2-- 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.Quotient8import Relation9import Set1011-- Equivalence classes and quotients are sets.  Both comprehensions12-- are bounded, so these definitions use only Separation and Power Set.13def equivalenceClass (A r x : Set) : Set := { y ∈ A | relates(r, x, y) }14def quotient (A r : Set) : Set := { C ∈ 𝒫(A) | ∃ x ∈ A, C = ⟦x⟧[A, r] }15notation infixl 70 "⧸" => quotient1617theorem equivalenceClass.subset (A r x : Set)18  shows (⟦x⟧[A, r] ⊆ A)19proof20  simp2122theorem equivalenceClass.self (A r x : Set)23  requires equivalence : Equivalence(A, r)24  requires hx : x ∈ A25  shows x ∈ ⟦x⟧[A, r]26proof27  apply equivalenceClass.membership.backward28  constructor29  exact hx30  exact Equivalence.reflexive with equivalence, x, hx3132theorem equivalenceClass.eq (A r x y : Set)33  requires equivalence : Equivalence(A, r)34  requires hx : x ∈ A35  requires hy : y ∈ A36  requires hxy : relates(r, x, y)37  shows ⟦x⟧[A, r] = ⟦y⟧[A, r]38proof39  ext z40  constructor41  intro hzx42  apply equivalenceClass.membership.backward43  simp [equivalenceClass.membership] at hzx44  rcases hzx with ⟨hzA, hxz⟩45  constructor46  exact hzA47  have symmetric := Equivalence.symmetric with equivalence, x, hx, y, hy, hxy48  exact Equivalence.transitive with equivalence, y, hy, x, hx, z, hzA, symmetric, hxz49  intro hzy50  apply equivalenceClass.membership.backward51  simp [equivalenceClass.membership] at hzy52  rcases hzy with ⟨hzA, hyz⟩53  constructor54  exact hzA55  exact Equivalence.transitive with equivalence, x, hx, y, hy, z, hzA, hxy, hyz5657theorem equivalenceClass.members_related (A r x y z : Set)58  requires equivalence : Equivalence(A, r)59  requires hx : x ∈ A60  requires hy : y ∈ ⟦x⟧[A, r]61  requires hz : z ∈ ⟦x⟧[A, r]62  shows relates(r, y, z)63proof64  obtain ⟨hyA, hxy⟩ := equivalenceClass.membership.forward with hy65  obtain ⟨hzA, hxz⟩ := equivalenceClass.membership.forward with hz66  have symmetric := Equivalence.symmetric with equivalence, x, hx, y, hyA, hxy67  exact Equivalence.transitive with equivalence, y, hyA, x, hx, z, hzA, symmetric, hxz6869theorem equivalenceClass.related_of_eq (A r x y : Set)70  requires equivalence : Equivalence(A, r)71  requires hx : x ∈ A72  requires hy : y ∈ A73  requires same : ⟦x⟧[A, r] = ⟦y⟧[A, r]74  shows relates(r, x, y)75proof76  have xSelf := equivalenceClass.self with equivalence, hx77  have ySelf := equivalenceClass.self with equivalence, hy78  rw ← same at ySelf79  exact equivalenceClass.members_related with equivalence, hx, xSelf, ySelf8081theorem quotient.contains_class (A r x : Set)82  requires equivalence : Equivalence(A, r)83  requires hx : x ∈ A84  shows ⟦x⟧[A, r] ∈ (A ⧸ r)85proof86  apply quotient.membership.backward87  constructor88  apply set.powerset.backward89  exact equivalenceClass.subset at A, r, x90  refine ⟨x, hx, rfl⟩9192theorem quotient.subset_powerset (A r : Set)93  shows ((A ⧸ r) ⊆ 𝒫(A))94proof95  simp with Subset9697theorem quotient.member_nonempty (C A r : Set)98  requires equivalence : Equivalence(A, r)99  requires hC : C ∈ (A ⧸ r)100  shows Nonempty(C)101proof102  simp [quotient.membership] at hC103  rcases hC with ⟨hCPower, x, hxA, hClass⟩104  witness x105  rw hClass106  exact equivalenceClass.self with equivalence, hxA107108theorem quotient.members_related (C A r y z : Set)109  requires equivalence : Equivalence(A, r)110  requires hC : C ∈ (A ⧸ r)111  requires hy : y ∈ C112  requires hz : z ∈ C113  shows relates(r, y, z)114proof115  obtain ⟨powerC, x, hxA, classShape⟩ := quotient.membership.forward with hC116  rw classShape at hy117  rw classShape at hz118  exact equivalenceClass.members_related with equivalence, hxA, hy, hz119120theorem quotient.class_of_member (C A r x : Set)121  requires equivalence : Equivalence(A, r)122  requires hC : C ∈ (A ⧸ r)123  requires hx : x ∈ C124  shows C = ⟦x⟧[A, r]125proof126  obtain ⟨powerC, y, hyA, classShape⟩ := quotient.membership.forward with hC127  rw classShape at hx128  obtain ⟨hxA, related⟩ := equivalenceClass.membership.forward with hx129  have classes := equivalenceClass.eq with equivalence, hyA, hxA, related130  rwa classShape131