Grace/Cumulus/Set/Relation.g17

Open in Workbench Download source

Imports

Finite

Declarations

Source

1-- Set-theoretic relations and functions2-- 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.Set.Relation8import Finite910-- (x, y) is the Kuratowski ordered pair.  The maplet alias x ↦ y is11-- reserved for entries of function-like graphs; both elaborate to orderedPair.12notation infixr 72 "↦" => orderedPair1314-- A generous set bound containing every Kuratowski pair drawn from A and B.15-- Separation then cuts out the Cartesian product.16def productBound (A B : Set) : Set := 𝒫(𝒫(A ∪ B))17def product (A B : Set) : Set := { p ∈ productBound(A, B) | ∃ x ∈ A, ∃ y ∈ B, p = (x, y) }18notation infixl 65 "×" => product1920-- Every coordinate occurring in a Kuratowski pair in r lies in union(union(r)).21def coordinateBound (r : Set) : Set := ⋃(⋃(r))22def domain (r : Set) : Set := { x ∈ coordinateBound(r) | ∃ y, (x, y) ∈ r }23def range (r : Set) : Set := { y ∈ coordinateBound(r) | ∃ x, (x, y) ∈ r }24def restrict (r A : Set) : Set := { p ∈ r | ∃ x ∈ A, ∃ y, p = (x, y) }2526predicate RelationBetween (r A B : Set) := (r ⊆ A × B)27predicate Functional (r : Set) := ∀ x, ∀ y, relates(r, x, y) → ∀ z, relates(r, x, z) → y = z28predicate FunctionBetween (r A B : Set) := RelationBetween(r, A, B) ∧ Functional(r) ∧ (∀ x ∈ A, ∃ y ∈ B, relates(r, x, y))2930-- A function from A to B is written f : A → B.31notation mixfix "_ : _ → _" => FunctionBetween3233theorem product.pair (x y A B : Set)34  requires hx : x ∈ A35  requires hy : y ∈ B36  shows (x, y) ∈ A × B37proof38  apply product.membership.backward39  constructor40  . unfold productBound41    apply set.powerset.backward42    intros z hz43    apply set.powerset.backward44    intros w hw45    simp [orderedPair, pair.membership] at hz46    cases hz with hsingle | hpair47    . rw hsingle at hw48      simp [pair.membership] at hw49      cases hw with hwx | hwx250      . rw hwx51        simp52      . rw hwx253        simp54    . rw hpair at hw55      simp [pair.membership] at hw56      cases hw with hwx | hwy57      . rw hwx58        simp59      . rw hwy60        simp61  . refine ⟨x, hx, y, hy, rfl⟩6263theorem product.monotone (A B C D : Set)64  requires hAC : A ⊆ C65  requires hBD : B ⊆ D66  shows (A × B ⊆ C × D)67proof68  intros p hp69  obtain ⟨bounded, x, hxA, y, hyB, pairShape⟩ := product.membership.forward with hp70  specialize hAC with x, hxA71  specialize hBD with y, hyB72  have pairIn := product.pair with hAC, hBD73  rwa pairShape7475theorem RelationBetween.monotone (r A B C D : Set)76  requires relation : RelationBetween(r, A, B)77  requires hAC : A ⊆ C78  requires hBD : B ⊆ D79  shows RelationBetween(r, C, D)80proof81  unfold RelationBetween at relation82  unfold RelationBetween83  have productSubset := product.monotone with hAC, hBD84  intros p hp85  specialize relation with p, hp86  exact productSubset with p, relation8788theorem orderedPair.first (a b c d : Set)89  requires h : (a, b) = (c, d)90  shows a = c91proof92  simp [orderedPair] at h93  have firstA := pair.left at {a, a}, {a, b}94  rw h at firstA95  simp [pair.membership] at firstA96  cases firstA with haa | hab97  have cMember := pair.left at c, c98  rw ← haa at cMember99  simp [pair.membership] at cMember100  cases cMember with hca | hca2101  simp102  simp103  have cMember := pair.left at c, d104  rw ← hab at cMember105  simp [pair.membership] at cMember106  cases cMember with hca | hca2107  simp108  simp109110theorem orderedPair.injective (a b c d : Set)111  requires h : (a, b) = (c, d)112  shows a = c ∧ b = d113proof114  constructor115  exact orderedPair.first with h116  have first := orderedPair.first with h117  rw first at h118  simp [orderedPair] at h119  have outer := pair.cancel_left with h120  exact pair.cancel_left with outer121122theorem range.contains (x y r : Set)123  requires hPair : (x, y) ∈ r124  shows y ∈ range(r)125proof126  apply range.membership.backward127  constructor128  unfold coordinateBound129  apply set.union.backward130  witness {x, y}131  constructor132  apply set.union.backward133  witness (x, y)134  constructor135  exact hPair136  simp [orderedPair, pair.membership]137  exact pair.right138  witness x139  exact hPair140141theorem range.empty142  shows range(∅) = ∅143proof144  ext y145  simp [range.membership, set.empty]146147theorem range.singleton_pair (x y : Set)148  shows range({(x, y)}) = {y}149proof150  ext z151  constructor152  intro hz153  simp [range.membership] at hz154  cases hz with hBound ∧ hWitness155  obtain ⟨source, hPair⟩ := hWitness156  have hOnlyPair := singleton.membership.forward with hPair157  have hCoordinates := orderedPair.injective with hOnlyPair158  cases hCoordinates with hSource ∧ hValue159  apply singleton.membership.backward160  exact hValue161  intro hz162  have hValue := singleton.membership.forward with hz163  rw hValue164  have hPair := singleton.self at (x, y)165  exact range.contains with hPair166167theorem range.pair_of_pairs (a b c d : Set)168  shows range({(a, b), (c, d)}) = {b, d}169proof170  ext z171  constructor172  . intro hz173    simp [range.membership] at hz174    obtain ⟨hBound, source, hPair⟩ := hz175    simp [pair.membership] at hPair176    cases hPair with hFirst | hSecond177    . obtain ⟨hSource, hValue⟩ := orderedPair.injective with hFirst178      rw hValue179      exact pair.left180    . obtain ⟨hSource, hValue⟩ := orderedPair.injective with hSecond181      rw hValue182      exact pair.right183  . intro hz184    simp [pair.membership] at hz185    cases hz with hFirst | hSecond186    . rw hFirst187      exact range.contains with (pair.left at (a, b), (c, d))188    . rw hSecond189      exact range.contains with (pair.right at (a, b), (c, d))190