Grace/Cumulus/Set/Function/Union.g17

Open in Workbench Download source

Imports

Image · Algebra

Declarations

Source

1-- The union of two functions with disjoint domains is a function on the2-- union of the domains; injectivity needs disjoint images too, and3-- surjectivity passes to the union of the codomains4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Set.Function.Union10import Image11import Algebra1213theorem union2.relates (f g x y : Set)14  shows relates(f ∪ g, x, y) ↔ relates(f, x, y) ∨ relates(g, x, y)15proof16  constructor17  . intro h18    have member : (x, y) ∈ f ∪ g := h19    have split := union2.membership.forward with member20    cases split with inF | inG21    . left22      exact inF23    . right24      exact inG25  . intro h26    cases h with inF | inG27    . have member : (x, y) ∈ f := inF28      exact union2.left at (x, y), f, g with member29    . have member : (x, y) ∈ g := inG30      exact union2.right at (x, y), f, g with member3132theorem FunctionBetween.union_disjoint (f g A B C D : Set)33  requires hf : f : A → C34  requires hg : g : B → D35  requires disjoint : Disjoint(A, B)36  shows f ∪ g : A ∪ B → C ∪ D37proof38  have fRelation := RelationBetween.monotone with (FunctionBetween.relation with hf), (union2.subset_left at A, B), (union2.subset_left at C, D)39  have gRelation := RelationBetween.monotone with (FunctionBetween.relation with hg), (union2.subset_right at A, B), (union2.subset_right at C, D)40  have separated := Disjoint.iff.forward with disjoint41  have fFunctional := FunctionBetween.functional with hf42  have gFunctional := FunctionBetween.functional with hg43  have fSubset : f ⊆ (A ∪ B) × (C ∪ D) := fRelation44  have gSubset : g ⊆ (A ∪ B) × (C ∪ D) := gRelation45  constructor46  . exact union2.subset with fSubset, gSubset47  . constructor48    . intros x y hxy z hxz49      have hxy2 := union2.relates.forward with hxy50      have hxz2 := union2.relates.forward with hxz51      cases hxy2 with fy | gy52      . cases hxz2 with fz | gz53        . exact fFunctional with x, y, fy, z, fz54        . exfalso55          have boundsY := FunctionBetween.bounds with hf, fy56          have boundsZ := FunctionBetween.bounds with hg, gz57          exact separated with x, boundsY.left, boundsZ.left58      . cases hxz2 with fz | gz59        . exfalso60          have boundsZ := FunctionBetween.bounds with hf, fz61          have boundsY := FunctionBetween.bounds with hg, gy62          exact separated with x, boundsZ.left, boundsY.left63        . exact gFunctional with x, y, gy, z, gz64    . intros x hx65      have split := union2.membership.forward with hx66      cases split with hxA | hxB67      . obtain ⟨y, hy, related⟩ := FunctionBetween.exists_value with hf, hxA68        refine ⟨y, (union2.subset_left at C, D with y, hy), ?_⟩69        apply union2.relates.backward70        left71        exact related72      . obtain ⟨y, hy, related⟩ := FunctionBetween.exists_value with hg, hxB73        refine ⟨y, (union2.subset_right at C, D with y, hy), ?_⟩74        apply union2.relates.backward75        right76        exact related7778theorem FunctionBetween.union_apply_left (f g A B C D x : Set)79  requires hf : f : A → C80  requires hg : g : B → D81  requires disjoint : Disjoint(A, B)82  requires hx : x ∈ A83  shows (f ∪ g)(x) = f(x)84proof85  have union := FunctionBetween.union_disjoint with hf, hg, disjoint86  have hxU := union2.subset_left at A, B with x, hx87  have related := FunctionBetween.relates_apply with hf, hx88  have lifted : relates(f ∪ g, x, f(x))89    apply union2.relates.backward90    left91    exact related92  exact FunctionBetween.apply_value with union, hxU, lifted9394theorem FunctionBetween.union_apply_right (f g A B C D x : Set)95  requires hf : f : A → C96  requires hg : g : B → D97  requires disjoint : Disjoint(A, B)98  requires hx : x ∈ B99  shows (f ∪ g)(x) = g(x)100proof101  have union := FunctionBetween.union_disjoint with hf, hg, disjoint102  have hxU := union2.subset_right at A, B with x, hx103  have related := FunctionBetween.relates_apply with hg, hx104  have lifted : relates(f ∪ g, x, g(x))105    apply union2.relates.backward106    right107    exact related108  exact FunctionBetween.apply_value with union, hxU, lifted109110theorem Injective.union_disjoint (f g A B C D : Set)111  requires hf : InjectiveBetween(f, A, C)112  requires hg : InjectiveBetween(g, B, D)113  requires domains : Disjoint(A, B)114  requires codomains : Disjoint(C, D)115  shows InjectiveBetween(f ∪ g, A ∪ B, C ∪ D)116proof117  have fFunction := Injective.function with hf118  have gFunction := Injective.function with hg119  have separated := Disjoint.iff.forward with codomains120  constructor121  . exact FunctionBetween.union_disjoint with fFunction, gFunction, domains122  . intros x hx y hy z hz hxz hyz123    have hxz2 := union2.relates.forward with hxz124    have hyz2 := union2.relates.forward with hyz125    cases hxz2 with fx | gx126    . cases hyz2 with fy | gy127      . have boundsX := FunctionBetween.bounds with fFunction, fx128        have boundsY := FunctionBetween.bounds with fFunction, fy129        exact hf.right with x, boundsX.left, y, boundsY.left, z, boundsX.right, fx, fy130      . exfalso131        have boundsX := FunctionBetween.bounds with fFunction, fx132        have boundsY := FunctionBetween.bounds with gFunction, gy133        exact separated with z, boundsX.right, boundsY.right134    . cases hyz2 with fy | gy135      . exfalso136        have boundsX := FunctionBetween.bounds with gFunction, gx137        have boundsY := FunctionBetween.bounds with fFunction, fy138        exact separated with z, boundsY.right, boundsX.right139      . have boundsX := FunctionBetween.bounds with gFunction, gx140        have boundsY := FunctionBetween.bounds with gFunction, gy141        exact hg.right with x, boundsX.left, y, boundsY.left, z, boundsX.right, gx, gy142143theorem Surjective.union_disjoint (f g A B C D : Set)144  requires hf : SurjectiveBetween(f, A, C)145  requires hg : SurjectiveBetween(g, B, D)146  requires domains : Disjoint(A, B)147  shows SurjectiveBetween(f ∪ g, A ∪ B, C ∪ D)148proof149  have fFunction := Surjective.function with hf150  have gFunction := Surjective.function with hg151  constructor152  . exact FunctionBetween.union_disjoint with fFunction, gFunction, domains153  . intros z hz154    have split := union2.membership.forward with hz155    cases split with hzC | hzD156    . obtain ⟨x, hx, related⟩ := hf.right with z, hzC157      refine ⟨x, (union2.subset_left at A, B with x, hx), ?_⟩158      apply union2.relates.backward159      left160      exact related161    . obtain ⟨x, hx, related⟩ := hg.right with z, hzD162      refine ⟨x, (union2.subset_right at A, B with x, hx), ?_⟩163      apply union2.relates.backward164      right165      exact related166167theorem Bijective.union_disjoint (f g A B C D : Set)168  requires hf : BijectiveBetween(f, A, C)169  requires hg : BijectiveBetween(g, B, D)170  requires domains : Disjoint(A, B)171  requires codomains : Disjoint(C, D)172  shows BijectiveBetween(f ∪ g, A ∪ B, C ∪ D)173proof174  constructor175  . exact Injective.union_disjoint with hf.left, hg.left, domains, codomains176  . exact Surjective.union_disjoint with hf.right, hg.right, domains177