Grace/Cumulus/Set/Function.g17

Open in Workbench Download source

Imports

Cumulus.Relation · Nat.Foundation

Declarations

Source

1-- Set-theoretic functions and bijections2-- 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.Function8import Cumulus.Relation9import Nat.Foundation1011predicate InjectiveBetween (f A B : Set) := FunctionBetween(f, A, B) ∧ (∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ B, relates(f, x, z) → relates(f, y, z) → x = y)12predicate SurjectiveBetween (f A B : Set) := FunctionBetween(f, A, B) ∧ (∀ y ∈ B, ∃ x ∈ A, relates(f, x, y))13predicate BijectiveBetween (f A B : Set) := InjectiveBetween(f, A, B) ∧ SurjectiveBetween(f, A, B)14predicate TotalBetween (f A B : Set) := ∀ x ∈ A, ∃ y ∈ B, relates(f, x, y)1516-- Graph of the identity function on A.17def identity (A : Set) : Set := { p ∈ A × A | ∃ x ∈ A, p = (x ↦ x) }1819-- The constant graph from A to B with value y.20def constantFunction (A B y : Set) : Set :=21  { p ∈ A × B | ∃ x ∈ A, p = (x ↦ y) }2223-- Graph of g after f. Explicit carrier sets keep every comprehension bounded.24def compose (g f A B C : Set) : Set := { p ∈ A × C | ∃ x ∈ A, ∃ y ∈ C, p = (x ↦ y) ∧ ∃ z ∈ B, relates(f, x, z) ∧ relates(g, z, y) }2526-- Pair two functions pointwise over their common domain.27def pairFunctions (f g A B C : Set) : Set :=28  { p ∈ A × (B × C) |29    ∃ x ∈ A, p = (x ↦ (f(x), g(x))) }3031def adjoinMap (f a b : Set) : Set := insert((a ↦ b), f)3233theorem adjoinMap.membership (p f a b : Set)34  shows p ∈ adjoinMap(f, a, b) ↔ (p = (a ↦ b) ∨ p ∈ f)35proof36  simp [adjoinMap, insert.membership]3738theorem constantFunction.relates (A B x y : Set)39  requires xInA : x ∈ A40  requires yInB : y ∈ B41  shows relates(constantFunction(A, B, y), x, y)42proof43  simp [relates, constantFunction.membership, product.pair]4445instance constantFunction.function (A B y : Set)46  requires yInB : y ∈ B47  shows constantFunction(A, B, y) : A → B48proof49  constructor50    intros p member51    obtain ⟨bounded, witnesses⟩ := constantFunction.membership.forward with member52    exact bounded53  . constructor54      intros x first xFirst second xSecond55      unfold relates at xFirst56      obtain ⟨_, i, iInA, firstShape⟩ := constantFunction.membership.forward with xFirst57      unfold relates at xSecond58      obtain ⟨_, j, jInA, secondShape⟩ := constantFunction.membership.forward with xSecond59      obtain ⟨_, firstEqual⟩ := orderedPair.injective with firstShape60      obtain ⟨_, secondEqual⟩ := orderedPair.injective with secondShape61      rw [firstEqual, secondEqual]62      rfl63    . intros x xInA64      refine ⟨y, yInB, (constantFunction.relates with xInA, yInB)⟩6566theorem FunctionBetween.relation (f A B : Set)67  requires h : f : A → B68  shows RelationBetween(f, A, B)69proof70  simp [FunctionBetween]7172theorem FunctionBetween.bounds (f A B x y : Set)73  requires h : f : A → B74  requires hxy : relates(f, x, y)75  shows x ∈ A ∧ y ∈ B76proof77  have relation := FunctionBetween.relation with h78  exact RelationBetween.bounds with relation, hxy7980theorem FunctionBetween.member_shape (f A B p : Set)81  requires h : f : A → B82  requires hp : p ∈ f83  shows ∃ x ∈ A, ∃ y ∈ B, p = (x, y) ∧ relates(f, x, y)84proof85  have relation := FunctionBetween.relation with h86  unfold RelationBetween at relation87  have bounded := relation with p, hp88  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with bounded89  refine ⟨x, hx, y, hy, shape, ?_⟩90  unfold relates91  rwa ← shape9293theorem FunctionBetween.functional (f A B : Set)94  requires h : f : A → B95  shows Functional(f)96proof97  simp [FunctionBetween]9899theorem FunctionBetween.empty (C : Set)100  shows ∅ : ∅ → C101proof102  simp [FunctionBetween, RelationBetween, Subset, Functional, relates, set.empty]103104theorem FunctionBetween.exists_value (f A B x : Set)105  requires h : f : A → B106  requires hx : x ∈ A107  shows ∃ y ∈ B, relates(f, x, y)108proof109  simp [FunctionBetween]110111theorem FunctionBetween.total (f A B : Set)112  requires h : f : A → B113  shows TotalBetween(f, A, B)114proof115  simp [FunctionBetween, TotalBetween]116117theorem FunctionBetween.foundation (f A B : Set)118  requires h : f : A → B119  shows functionOn(f, A, B)120proof121  rcases h with ⟨relation, functional, total⟩122  constructor123  . intros input hInput124    specialize total with input, hInput125    obtain ⟨output, outputB, mapped⟩ := total126    witness output127    constructor128    exact outputB129    constructor130    exact mapped131    intros other mappedOther132    specialize functional with input, output, mapped, other, mappedOther133    rw functional134    rfl135  . intros p hp136    unfold RelationBetween at relation137    specialize relation with p, hp138    obtain ⟨bounded, x, hxA, y, hyB, shape⟩ := product.membership.forward with relation139    refine ⟨x, y, hxA, hyB, shape⟩140141theorem FunctionBetween.apply_value (f A B x y : Set)142  requires h : f : A → B143  requires hx : x ∈ A144  requires hxy : relates(f, x, y)145  shows f(x) = y146proof147  apply function.apply at f, A, B, x, y148  constructor149  . have foundation := FunctionBetween.foundation at f, A, B150    exact foundation with h151  refine ⟨hx, hxy⟩152153theorem FunctionBetween.apply_closed (f A B x : Set)154  requires function : f : A → B155  requires input : x ∈ A156  shows f(x) ∈ B157proof158  obtain ⟨y, output, mapped⟩ := FunctionBetween.exists_value with function, input159  have value := FunctionBetween.apply_value with function, input, mapped160  rwa value161162theorem constantFunction.apply (A B x y : Set)163  requires xInA : x ∈ A164  requires yInB : y ∈ B165  shows apply(constantFunction(A, B, y), x) = y166proof167  have function := constantFunction.function at A, B, y with yInB168  have mapped := constantFunction.relates with xInA, yInB169  exact FunctionBetween.apply_value with function, xInA, mapped170171theorem FunctionBetween.relates_apply (f A B x : Set)172  requires function : f : A → B173  requires input : x ∈ A174  shows relates(f, x, f(x))175proof176  obtain ⟨y, output, mapped⟩ := FunctionBetween.exists_value with function, input177  have value := FunctionBetween.apply_value with function, input, mapped178  rwa value179180-- A graph can be given a smaller codomain once all its values are181-- known to lie there. This is particularly useful for sequences in a set.182theorem FunctionBetween.codomain_of_values (f A B C : Set)183  requires function : f : A → B184  requires values : ∀ x ∈ A, f(x) ∈ C185  shows f : A → C186proof187  constructor188    intros p member189    obtain ⟨x, memberA, y, memberB, shape, related⟩ := FunctionBetween.member_shape with function, member190    have value := FunctionBetween.apply_value with function, memberA, related191    have memberC := values with x, memberA192    rw value at memberC193    rw shape194    exact product.pair with memberA, memberC195  . constructor196    . exact FunctionBetween.functional with function197    . intros x memberA198      refine ⟨f(x), (values with x, memberA), (FunctionBetween.relates_apply with function, memberA)⟩199200theorem pairFunctions.relates (f g A B C x : Set)201  requires fFunction : f : A → B202  requires gFunction : g : A → C203  requires input : x ∈ A204  shows relates(pairFunctions(f, g, A, B, C), x,205    (f(x), g(x)))206proof207  have fValue := FunctionBetween.apply_closed with fFunction, input208  have gValue := FunctionBetween.apply_closed with gFunction, input209  have pairValue := product.pair with fValue, gValue210  unfold relates211  apply pairFunctions.membership.backward212  constructor213  . exact product.pair at x, (f(x), g(x)), A, B × C with214      input, pairValue215  . refine ⟨x, input, rfl⟩216217instance pairFunctions.function (f g A B C : Set)218  requires fFunction : f : A → B219  requires gFunction : g : A → C220  shows pairFunctions(f, g, A, B, C) : A → B × C221proof222  constructor223    intros p member224    obtain ⟨bounded, witnesses⟩ := pairFunctions.membership.forward with member225    exact bounded226  . constructor227      intros x y xy z xz228      unfold relates at xy229      obtain ⟨_, a, aInA, firstShape⟩ := pairFunctions.membership.forward with xy230      unfold relates at xz231      obtain ⟨_, b, bInA, secondShape⟩ := pairFunctions.membership.forward with xz232      obtain ⟨sameA, shapeY⟩ := orderedPair.injective with firstShape233      obtain ⟨sameB, shapeZ⟩ := orderedPair.injective with secondShape234      cc235    . intros x input236      have fValue := FunctionBetween.apply_closed with fFunction, input237      have gValue := FunctionBetween.apply_closed with gFunction, input238      refine ⟨(f(x), g(x)), (product.pair with fValue, gValue), (pairFunctions.relates with fFunction, gFunction, input)⟩239240theorem pairFunctions.apply (f g A B C x : Set)241  requires fFunction : f : A → B242  requires gFunction : g : A → C243  requires input : x ∈ A244  shows apply(pairFunctions(f, g, A, B, C), x) =245    (f(x), g(x))246proof247  have function := pairFunctions.function with fFunction, gFunction248  have mapped := pairFunctions.relates with fFunction, gFunction, input249  exact FunctionBetween.apply_value with function, input, mapped250251theorem Functional.unique (f x y z : Set)252  requires hf : Functional(f)253  requires hxy : relates(f, x, y)254  requires hxz : relates(f, x, z)255  shows y = z256proof257  exact hf with x, y, hxy, z, hxz258259theorem TotalBetween.predecessor (f A : Set, n : Nat)260  requires h : TotalBetween(f, succ(n), A)261  shows TotalBetween(f, n, A)262proof263  simp [TotalBetween]264265theorem identity.relation (A : Set)266  shows RelationBetween(identity(A), A, A)267proof268  simp [RelationBetween, Subset]269270theorem identity.relates (x A : Set)271  requires hx : x ∈ A272  shows relates(identity(A), x, x)273proof274  simp [relates, identity.membership, product.pair]275276theorem identity.total (A : Set)277  shows TotalBetween(identity(A), A, A)278proof279  simp [TotalBetween, identity.relates]280281theorem identity.functional (A : Set)282  shows Functional(identity(A))283proof284  intros x y hxy z hxz285  unfold relates at hxy286  simp [identity] at hxy287  rcases hxy with ⟨hxyProduct, a, haA, hxyPair⟩288  unfold relates at hxz289  simp [identity] at hxz290  rcases hxz with ⟨hxzProduct, b, hbA, hxzPair⟩291  obtain ⟨hxa, hya⟩ := orderedPair.injective with hxyPair292  obtain ⟨hxb, hzb⟩ := orderedPair.injective with hxzPair293  rw [hya, hzb]294  rwa ← hxa295296instance identity.function (A : Set)297  shows identity(A) : A → A298proof299  constructor300  exact identity.relation301  constructor302  exact identity.functional303  exact identity.total at A304305theorem identity.apply (x A : Set)306  requires member : x ∈ A307  shows apply(identity(A), x) = x308proof309  have function := identity.function at A310  have mapped := identity.relates with member311  exact FunctionBetween.apply_value with function, member, mapped312313theorem identity.injective (A : Set)314  shows InjectiveBetween(identity(A), A, A)315proof316  constructor317  exact identity.function318  intros x hx y hy z hz hxz hyz319  unfold relates at hxz320  simp [identity] at hxz321  rcases hxz with ⟨hxzProduct, a, haA, hxzPair⟩322  obtain ⟨hxa, hza⟩ := orderedPair.injective with hxzPair323  unfold relates at hyz324  simp [identity] at hyz325  rcases hyz with ⟨hyzProduct, b, hbA, hyzPair⟩326  obtain ⟨hyb, hzb⟩ := orderedPair.injective with hyzPair327  rw [hxa, hyb]328  rwa ← hza329330theorem identity.surjective (A : Set)331  shows SurjectiveBetween(identity(A), A, A)332proof333  simp [SurjectiveBetween, identity.function, identity.relates]334335theorem identity.bijective (A : Set)336  shows BijectiveBetween(identity(A), A, A)337proof338  refine ⟨identity.injective at A, identity.surjective at A⟩339340theorem compose.relation (g f A B C : Set)341  shows RelationBetween(compose(g, f, A, B, C), A, C)342proof343  simp [RelationBetween, Subset]344345theorem compose.relates (g f A B C x z y : Set)346  requires hx : x ∈ A347  requires hz : z ∈ B348  requires hy : y ∈ C349  requires hf : relates(f, x, z)350  requires hg : relates(g, z, y)351  shows relates(compose(g, f, A, B, C), x, y)352proof353  unfold relates354  apply compose.membership.backward355  constructor356  exact product.pair with hx, hy357  refine ⟨x, hx, y, hy, rfl, z, hz, hf, hg⟩358359theorem compose.total (g f A B C : Set)360  requires hf : f : A → B361  requires hg : g : B → C362  shows TotalBetween(compose(g, f, A, B, C), A, C)363proof364  intros x hx365  obtain ⟨z, hzB, hfxz⟩ := FunctionBetween.exists_value with hf, hx366  obtain ⟨y, hyC, hgzy⟩ := FunctionBetween.exists_value with hg, hzB367  witness y368  constructor369  exact hyC370  exact compose.relates with hx, hzB, hyC, hfxz, hgzy371372theorem compose.functional (g f A B C : Set)373  requires hf : f : A → B374  requires hg : g : B → C375  shows Functional(compose(g, f, A, B, C))376proof377  intros x y hxy z hxz378  unfold relates at hxy379  simp [compose] at hxy380  rcases hxy with ⟨hxyProduct, x1, hx1A, y1, hy1C, hpair1, m, hmB, hfxm, hgmy⟩381  obtain ⟨hxx1, hyy1⟩ := orderedPair.injective with hpair1382  rw ← hxx1 at hfxm383  rw ← hyy1 at hgmy384  unfold relates at hxz385  simp [compose] at hxz386  rcases hxz with ⟨hxzProduct, x2, hx2A, z2, hz2C, hpair2, n, hnB, hfxn, hgnz⟩387  obtain ⟨hxx2, hzz2⟩ := orderedPair.injective with hpair2388  rw ← hxx2 at hfxn389  rw ← hzz2 at hgnz390  have fUnique := FunctionBetween.functional with hf, x, m, hfxm, n, hfxn391  rw ← fUnique at hgnz392  have gUnique := FunctionBetween.functional with hg393  exact gUnique with m, y, hgmy, z, hgnz394395instance compose.function (g f A B C : Set)396  requires hf : f : A → B397  requires hg : g : B → C398  shows compose(g, f, A, B, C) : A → C399proof400  constructor401  exact compose.relation402  constructor403  exact compose.functional with hf, hg404  exact compose.total with hf, hg405406theorem compose.apply (g f A B C x : Set)407  requires fFunction : f : A → B408  requires gFunction : g : B → C409  requires input : x ∈ A410  shows apply(compose(g, f, A, B, C), x) = g(f(x))411proof412  have middle := FunctionBetween.apply_closed with fFunction, input413  have output := FunctionBetween.apply_closed with gFunction, middle414  have mappedF := FunctionBetween.relates_apply with fFunction, input415  have mappedG := FunctionBetween.relates_apply with gFunction, middle416  have mapped := compose.relates with input, middle, output, mappedF, mappedG417  have function := compose.function with fFunction, gFunction418  exact FunctionBetween.apply_value with function, input, mapped419420-- Image and corestriction do not change the function graph.421def functionImage (f A B : Set) : Set := { y ∈ B | ∃ x ∈ A, y = f(x) }422423theorem functionImage.subset (f A B : Set)424  shows functionImage(f, A, B) ⊆ B425proof426  simp427428theorem functionImage.value (f A B x : Set)429  requires function : f : A → B430  requires hx : x ∈ A431  shows f(x) ∈ functionImage(f, A, B)432proof433  have valueIn := FunctionBetween.apply_closed with *434  exact functionImage.membership.backward with ⟨valueIn, x, hx, rfl⟩435436theorem identity.inclusion (A B : Set)437  requires subset : A ⊆ B438  shows identity(A) : A → B439proof440  have function := identity.function at A441  have values : ∀ x ∈ A, identity(A)(x) ∈ B by simp [identity.apply]442  exact FunctionBetween.codomain_of_values with function, values443444theorem functionImage.identity (A B : Set)445  requires subset : A ⊆ B446  shows functionImage(identity(A), A, B) = A447proof448  have function := identity.inclusion with subset449  ext x450  constructor451  . intro member452    obtain ⟨inB, a, ha, value⟩ := functionImage.membership.forward with member453    have equal := identity.apply with ha454    rw value455    rwa equal456  . intro member457    have image := functionImage.value with *458    have equal := identity.apply with member459    rwa equal at image460461theorem functionImage.corestrict (f A B : Set)462  requires function : f : A → B463  shows f : A → functionImage(f, A, B)464proof465  apply FunctionBetween.codomain_of_values with function466  intros x hx467  exact functionImage.value with *468469theorem functionImage.surjective (f A B : Set)470  requires function : f : A → B471  shows SurjectiveBetween(f, A, functionImage(f, A, B))472proof473  have corestricted := functionImage.corestrict with *474  unfold SurjectiveBetween475  refine ⟨corestricted, ?_⟩476  intros y hy477  obtain ⟨yIn, x, hx, shape⟩ := functionImage.membership.forward with hy478  have edge := FunctionBetween.relates_apply at f, A, B, x with *479  refine ⟨x, hx, ?_⟩480  rwa shape481482theorem restrict.relates (f S x y : Set)483  shows relates(restrict(f, S), x, y) ↔ x ∈ S ∧ relates(f, x, y)484proof485  constructor486  . intro edge487    unfold relates at edge488    obtain ⟨original, u, hu, v, shape⟩ := restrict.membership.forward with edge489    have coordinates := orderedPair.injective with shape490    have member : x ∈ S by rwa coordinates.left491    refine ⟨member, ?_⟩492    exact original493  . intro data494    unfold relates495    apply restrict.membership.backward496    have original := data.right497    refine ⟨original, x, data.left, y, rfl⟩498499theorem restrict.nested (f S T : Set)500  requires subset : S ⊆ T501  shows restrict(restrict(f, T), S) = restrict(f, S)502proof503  ext p504  constructor505  . intro member506    obtain ⟨inside, x, inS, y, shape⟩ := restrict.membership.forward with member507    have original := restrict.membership.forward with inside508    exact restrict.membership.backward with ⟨original.left, x, inS, y, shape⟩509  . intro member510    obtain ⟨inside, x, inS, y, shape⟩ := restrict.membership.forward with member511    have inT := subset with x, inS512    have restricted : p ∈ restrict(f, T) := restrict.membership.backward with ⟨inside, x, inT, y, shape⟩513    exact restrict.membership.backward with ⟨restricted, x, inS, y, shape⟩514515theorem restrict.function (f A B S C : Set)516  requires function : f : A → B517  requires subset : S ⊆ A518  requires closed : ∀ x ∈ S, f(x) ∈ C519  shows restrict(f, S) : S → C520proof521  have relation := FunctionBetween.relation with function522  have functional := FunctionBetween.functional with function523  unfold FunctionBetween524  refine ⟨?_, ⟨?_, ?_⟩⟩525    intros p hp526    obtain ⟨original, x, hx, y, shape⟩ := restrict.membership.forward with hp527    have xIn := subset with x, hx528    have edge : relates(f, x, y)529      unfold relates530      rwa ← shape531    have value := FunctionBetween.apply_value with *532    have yIn := closed with x, hx533    rw value at yIn534    rw shape535    exact product.pair with *536    intros x y left z right537    have first := restrict.relates.forward with left538    have second := restrict.relates.forward with right539    exact Functional.unique with functional, first.right, second.right540  . intros x hx541    have xIn := subset with x, hx542    have yIn := closed with x, hx543    have edge := FunctionBetween.relates_apply with *544    refine ⟨f(x), yIn, ?_⟩545    exact restrict.relates.backward with ⟨hx, edge⟩546547theorem restrict.apply (f A B S C x : Set)548  requires function : f : A → B549  requires subset : S ⊆ A550  requires closed : ∀ x ∈ S, f(x) ∈ C551  requires hx : x ∈ S552  shows restrict(f, S)(x) = f(x)553proof554  have restricted := restrict.function with *555  have xIn := subset with x, hx556  have original := FunctionBetween.relates_apply at f, A, B, x with *557  have edge : relates(restrict(f, S), x, f(x)) := restrict.relates.backward with ⟨hx, original⟩558  exact FunctionBetween.apply_value with *559560-- Restricting only the domain needs no extra codomain closure obligation.561theorem restrict.domain_function (f A B S : Set)562  requires function : f : A → B563  requires subset : S ⊆ A564  shows restrict(f, S) : S → B565proof566  have closed : ∀ x ∈ S, f(x) ∈ B567    intros x hx568    have member := subset with x, hx569    exact FunctionBetween.apply_closed with function, member570  exact restrict.function with function, subset, closed571572theorem restrict.domain_apply (f A B S x : Set)573  requires function : f : A → B574  requires subset : S ⊆ A575  requires member : x ∈ S576  shows restrict(f, S)(x) = f(x)577proof578  have closed : ∀ y ∈ S, f(y) ∈ B579    intros y hy580    have inA := subset with y, hy581    exact FunctionBetween.apply_closed with function, inA582  exact restrict.apply with function, subset, closed, member583584-- Functions with the same domain and pointwise values are the same graph.585theorem FunctionBetween.subset_of_agree (f g A B : Set)586  requires hf : f : A → B587  requires hg : g : A → B588  requires same : ∀ x ∈ A, f(x) = g(x)589  shows f ⊆ g590proof591  intros p hp592  obtain ⟨x, hx, y, hy, shape, edge⟩ := FunctionBetween.member_shape with hf, hp593  have value := FunctionBetween.apply_value with *594  have equal := same with x, hx595  have image := FunctionBetween.relates_apply at g, A, B, x with *596  have result : relates(g, x, y) by cc597  unfold relates at result598  rwa shape599600theorem FunctionBetween.ext (f g A B : Set)601  requires hf : f : A → B602  requires hg : g : A → B603  requires same : ∀ x ∈ A, f(x) = g(x)604  shows f = g605proof606  have fg := FunctionBetween.subset_of_agree with hf, hg, same607  have reversed : ∀ x ∈ A, g(x) = f(x) by simp608  have gf := FunctionBetween.subset_of_agree with hg, hf, reversed609  ext p610  simp611612theorem compose.identity_left (f A B : Set)613  requires hf : f : A → B614  shows compose(identity(B), f, A, B, B) = f615proof616  ext p617  constructor618  intro hp619  simp [compose] at hp620  rcases hp with ⟨_, x, hxA, y, hyB, hpair, z, hzB, hfxz, hidzy⟩621  have self := identity.relates with hzB622  have unique := identity.functional at B with z, y, hidzy, z, self623  unfold relates at hfxz624  rw hpair625  rwa unique626  intro hp627  obtain ⟨x2, hxA, y2, hyB, hpair, hrel⟩ := FunctionBetween.member_shape with hf, hp628  have hid := identity.relates with hyB629  have composed := compose.relates with hxA, hyB, hyB, hrel, hid630  unfold relates at composed631  rwa ← hpair at composed632633theorem compose.identity_right (f A B : Set)634  requires hf : f : A → B635  shows compose(f, identity(A), A, A, B) = f636proof637  ext p638  constructor639  intro hp640  simp [compose] at hp641  rcases hp with ⟨_, x, hxA, y, hyB, hpair, z, hzA, hidxz, hfzy⟩642  have self := identity.relates with hxA643  have unique := identity.functional at A with x, z, hidxz, x, self644  rw hpair645  rwa unique at hfzy646  intro hp647  obtain ⟨x2, hxA, y2, hyB, hpair, hrel⟩ := FunctionBetween.member_shape with hf, hp648  have hid := identity.relates with hxA649  have composed := compose.relates with hxA, hxA, hyB, hid, hrel650  unfold relates at composed651  rwa ← hpair at composed652653theorem Injective.function (f A B : Set)654  requires h : InjectiveBetween(f, A, B)655  shows f : A → B656proof657  rcases h with ⟨fn, injective⟩658  exact fn659660theorem Surjective.function (f A B : Set)661  requires h : SurjectiveBetween(f, A, B)662  shows f : A → B663proof664  rcases h with ⟨fn, surjective⟩665  exact fn666667theorem Bijective.injective (f A B : Set)668  requires h : BijectiveBetween(f, A, B)669  shows InjectiveBetween(f, A, B)670proof671  rcases h with ⟨injective, surjective⟩672  exact injective673674theorem Bijective.surjective (f A B : Set)675  requires h : BijectiveBetween(f, A, B)676  shows SurjectiveBetween(f, A, B)677proof678  rcases h with ⟨injective, surjective⟩679  exact surjective680681theorem Injective.cancel (f A B x y z : Set)682  requires injective : InjectiveBetween(f, A, B)683  requires hx : x ∈ A684  requires hy : y ∈ A685  requires hz : z ∈ B686  requires hxz : relates(f, x, z)687  requires hyz : relates(f, y, z)688  shows x = y689proof690  rcases injective with (fn, cancel)691  exact cancel with x, hx, y, hy, z, hz, hxz, hyz692693theorem converse.function_of_bijective (f A B : Set)694  requires h : BijectiveBetween(f, A, B)695  shows converse(f, A, B) : B → A696proof697  constructor698  exact converse.relation699  constructor700  intros y x hyx z hyz701  obtain ⟨hyB, hxA⟩ := converse.bounds with hyx702  obtain ⟨hyB2, hzA⟩ := converse.bounds with hyz703  have hxy := converse.reflects with hyx704  have hzy := converse.reflects with hyz705  obtain ⟨fn, injectiveLaw⟩ := Bijective.injective with h706  exact injectiveLaw with x, hxA, z, hzA, y, hyB, hxy, hzy707  intros y hy708  obtain ⟨fn, surjectiveLaw⟩ := Bijective.surjective with h709  specialize surjectiveLaw with y, hy710  obtain ⟨preimage, hpreimageA, hpreimageY⟩ := surjectiveLaw711  witness preimage712  constructor713  exact hpreimageA714  exact converse.relates with hpreimageA, hy, hpreimageY715716theorem converse.injective_of_bijective (f A B : Set)717  requires h : BijectiveBetween(f, A, B)718  shows InjectiveBetween(converse(f, A, B), B, A)719proof720  constructor721  exact converse.function_of_bijective with h722  intros y hy z hz x hx hyx hzx723  have hxy := converse.reflects with hyx724  have hxz := converse.reflects with hzx725  have injective := Bijective.injective with h726  have fn := Injective.function with injective727  have functional := FunctionBetween.functional with fn728  exact functional with x, y, hxy, z, hxz729730theorem converse.surjective_of_bijective (f A B : Set)731  requires h : BijectiveBetween(f, A, B)732  shows SurjectiveBetween(converse(f, A, B), B, A)733proof734  constructor735  exact converse.function_of_bijective with h736  intros x hx737  have injective := Bijective.injective with h738  have fn := Injective.function with injective739  obtain ⟨y, hyB, hxy⟩ := FunctionBetween.exists_value with fn, hx740  witness y741  constructor742  exact hyB743  exact converse.relates with hx, hyB, hxy744745theorem converse.bijective (f A B : Set)746  requires h : BijectiveBetween(f, A, B)747  shows BijectiveBetween(converse(f, A, B), B, A)748proof749  simp [BijectiveBetween, converse.injective_of_bijective, converse.surjective_of_bijective]750751theorem Bijective.inverse_apply (f A B x : Set)752  requires bijective : BijectiveBetween(f, A, B)753  requires hx : x ∈ A754  shows converse(f, A, B)(f(x)) = x755proof756  have injective := Bijective.injective with bijective757  have function := Injective.function with injective758  have inverse := converse.function_of_bijective with bijective759  have fx := FunctionBetween.apply_closed with function, hx760  have edge := FunctionBetween.relates_apply with function, hx761  have reverse := converse.relates with *762  exact FunctionBetween.apply_value with *763764theorem Bijective.apply_inverse (f A B y : Set)765  requires bijective : BijectiveBetween(f, A, B)766  requires hy : y ∈ B767  shows f(converse(f, A, B)(y)) = y768proof769  have injective := Bijective.injective with bijective770  have function := Injective.function with injective771  have inverse := converse.function_of_bijective with bijective772  have preimage := FunctionBetween.apply_closed with inverse, hy773  have edge := FunctionBetween.relates_apply with inverse, hy774  have original := converse.reflects with edge775  exact FunctionBetween.apply_value with *776777theorem compose.factors (g f A B C x y : Set)778  requires h : relates(compose(g, f, A, B, C), x, y)779  shows ∃ z ∈ B, relates(f, x, z) ∧ relates(g, z, y)780proof781  unfold relates at h782  simp [compose.membership] at h783  rcases h with ⟨hProduct, a, haA, b, hbC, hPair, z, hzB, hfaz, hgzb⟩784  obtain (hxa, hyb) := orderedPair.injective with hPair785  rw ← hxa at hfaz786  rw ← hyb at hgzb787  refine ⟨z, hzB, hfaz, hgzb⟩788789theorem compose.injective (g f A B C : Set)790  requires hf : InjectiveBetween(f, A, B)791  requires hg : InjectiveBetween(g, B, C)792  shows InjectiveBetween(compose(g, f, A, B, C), A, C)793proof794  constructor795  have fFunction := Injective.function with hf796  have gFunction := Injective.function with hg797  exact compose.function with fFunction, gFunction798  intros x hx y hy w hw hxw hyw799  obtain ⟨m, hmB, hfxm, hgmw⟩ := compose.factors with hxw800  obtain ⟨n, hnB, hfyn, hgnw⟩ := compose.factors with hyw801  have middleEqual := Injective.cancel with hg, hmB, hnB, hw, hgmw, hgnw802  rw ← middleEqual at hfyn803  exact Injective.cancel with hf, hx, hy, hmB, hfxm, hfyn804805theorem compose.surjective (g f A B C : Set)806  requires hf : BijectiveBetween(f, A, B)807  requires hg : BijectiveBetween(g, B, C)808  shows SurjectiveBetween(compose(g, f, A, B, C), A, C)809proof810  constructor811  have fInjective := Bijective.injective with hf812  have fFunction := Injective.function with fInjective813  have gInjective := Bijective.injective with hg814  have gFunction := Injective.function with gInjective815  exact compose.function with fFunction, gFunction816  intros y hy817  obtain (gFunction2, gOnto) := Bijective.surjective with hg818  specialize gOnto with y, hy819  obtain ⟨z, hzB, hgzy⟩ := gOnto820  obtain (fFunction2, fOnto) := Bijective.surjective with hf821  specialize fOnto with z, hzB822  obtain ⟨x, hxA, hfxz⟩ := fOnto823  witness x824  constructor825  exact hxA826  exact compose.relates with hxA, hzB, hy, hfxz, hgzy827828theorem compose.bijective (g f A B C : Set)829  requires hf : BijectiveBetween(f, A, B)830  requires hg : BijectiveBetween(g, B, C)831  shows BijectiveBetween(compose(g, f, A, B, C), A, C)832proof833  --! Reduce bijectivity to its two components.834  --| The two obligations can be discharged independently.835  constructor836  . --! Injectivity837    --| Equality after composition is pulled back through g and then f.838    have fInjective := Bijective.injective with hf839    have gInjective := Bijective.injective with hg840    exact compose.injective with fInjective, gInjective841  . --! Surjectivity842    --| An output is pulled back through g and then through f.843    exact compose.surjective with hf, hg844845theorem adjoinMap.relation (f A B a b : Set)846  requires hf : f : A → B847  shows RelationBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))848proof849  intros p hp850  have shape := adjoinMap.membership.forward with hp851  cases shape with newPair | oldPair852  rw newPair853  apply product.pair854  exact insert.self855  exact insert.self856  have relation := FunctionBetween.relation with hf857  unfold RelationBetween at relation858  specialize relation with p, oldPair859  obtain ⟨oldBound, x, hxA, y, hyB, pairShape⟩ := product.membership.forward with relation860  rw pairShape861  apply product.pair862  exact insert.contains with hxA863  exact insert.contains with hyB864865theorem adjoinMap.relates_new (f a b : Set)866  shows relates(adjoinMap(f, a, b), a, b)867proof868  simp [relates]869870theorem adjoinMap.relates_old (f a b x y : Set)871  requires h : relates(f, x, y)872  shows relates(adjoinMap(f, a, b), x, y)873proof874  simp [relates]875876theorem adjoinMap.functional (f A B a b : Set)877  requires hf : f : A → B878  requires ha : ¬a ∈ A879  shows Functional(adjoinMap(f, a, b))880proof881  intros x y hxy z hxz882  unfold relates at hxy883  unfold relates at hxz884  have firstShape := adjoinMap.membership.forward with hxy885  have secondShape := adjoinMap.membership.forward with hxz886  cases firstShape with firstNew | firstOld887  . cases secondShape with secondNew | secondOld888    . obtain (xIsA, yIsB) := orderedPair.injective with firstNew889      obtain (xIsAAgain, zIsB) := orderedPair.injective with secondNew890      rw [yIsB, zIsB]891      rfl892    . obtain (xIsA, yIsB) := orderedPair.injective with firstNew893      have oldRelates := relates.backward with secondOld894      obtain (xInA, zInB) := FunctionBetween.bounds with hf, oldRelates895      rw xIsA at xInA896      contradiction897  . cases secondShape with secondNew | secondOld898    . obtain (xIsA, zIsB) := orderedPair.injective with secondNew899      have oldRelates := relates.backward with firstOld900      obtain (xInA, yInB) := FunctionBetween.bounds with hf, oldRelates901      rw xIsA at xInA902      contradiction903    . have oldFunctional := FunctionBetween.functional with hf904      have firstRelates := relates.backward with firstOld905      have secondRelates := relates.backward with secondOld906      exact oldFunctional with x, y, firstRelates, z, secondRelates907908theorem adjoinMap.total (f A B a b : Set)909  requires hf : f : A → B910  shows TotalBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))911proof912  intros x hx913  have sourceShape := insert.membership.forward with hx914  cases sourceShape with isNew | isOld915  witness b916  constructor917  exact insert.self918  rw isNew919  exact adjoinMap.relates_new920  obtain ⟨y, hyB, hxy⟩ := FunctionBetween.exists_value with hf, isOld921  witness y922  constructor923  exact insert.contains with hyB924  exact adjoinMap.relates_old with hxy925926theorem adjoinMap.function (f A B a b : Set)927  requires hf : f : A → B928  requires ha : ¬a ∈ A929  shows adjoinMap(f, a, b) : insert(a, A) → insert(b, B)930proof931  constructor932  exact adjoinMap.relation with hf933  constructor934  exact adjoinMap.functional with hf, ha935  exact adjoinMap.total at f, A, B, a, b with hf936937theorem adjoinMap.injective (f A B a b : Set)938  requires hf : InjectiveBetween(f, A, B)939  requires ha : ¬a ∈ A940  requires hb : ¬b ∈ B941  shows InjectiveBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))942proof943  have oldFunction := Injective.function with hf944  constructor945  . exact adjoinMap.function with oldFunction, ha946  . intros x hx y hy z hz hxz hyz947    unfold relates at hxz948    unfold relates at hyz949    have firstShape := adjoinMap.membership.forward with hxz950    have secondShape := adjoinMap.membership.forward with hyz951    cases firstShape with firstNew | firstOld952    . cases secondShape with secondNew | secondOld953      . obtain (xIsA, zIsB) := orderedPair.injective with firstNew954        obtain (yIsA, zIsBAgain) := orderedPair.injective with secondNew955        rw [xIsA, yIsA]956        rfl957      . obtain (xIsA, zIsB) := orderedPair.injective with firstNew958        have oldRelates := relates.backward with secondOld959        obtain (yInA, zInB) := FunctionBetween.bounds with oldFunction, oldRelates960        rw zIsB at zInB961        contradiction962    . cases secondShape with secondNew | secondOld963      . obtain (yIsA, zIsB) := orderedPair.injective with secondNew964        have oldRelates := relates.backward with firstOld965        obtain (xInA, zInB) := FunctionBetween.bounds with oldFunction, oldRelates966        rw zIsB at zInB967        contradiction968      . have firstRelates := relates.backward with firstOld969        have secondRelates := relates.backward with secondOld970        have xOld := insert.membership.forward with hx971        cases xOld with xWasNew | xInA972        . rw xWasNew at firstRelates973          obtain (aInA, zBound) := FunctionBetween.bounds with oldFunction, firstRelates974          contradiction975        . have yOld := insert.membership.forward with hy976          cases yOld with yWasNew | yInA977          . rw yWasNew at secondRelates978            obtain (aInA, zBound) := FunctionBetween.bounds with oldFunction, secondRelates979            contradiction980          . have zOld := insert.membership.forward with hz981            cases zOld with zWasNew | zInB982            . rw zWasNew at firstRelates983              obtain (xBound, bInB) := FunctionBetween.bounds with oldFunction, firstRelates984              contradiction985            . exact Injective.cancel with hf, xInA, yInA, zInB, firstRelates, secondRelates986987theorem adjoinMap.surjective (f A B a b : Set)988  requires hf : SurjectiveBetween(f, A, B)989  requires ha : ¬a ∈ A990  shows SurjectiveBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))991proof992  constructor993  have oldFunction := Surjective.function with hf994  exact adjoinMap.function with oldFunction, ha995  intros y hy996  have targetShape := insert.membership.forward with hy997  cases targetShape with isNew | isOld998  witness a999  constructor1000  exact insert.self1001  rw isNew1002  exact adjoinMap.relates_new1003  rcases hf with (oldFunctionAgain, oldOnto)1004  specialize oldOnto with y, isOld1005  obtain ⟨x, hxA, hxy⟩ := oldOnto1006  witness x1007  constructor1008  exact insert.contains with hxA1009  exact adjoinMap.relates_old with hxy10101011theorem adjoinMap.bijective (f A B a b : Set)1012  requires hf : BijectiveBetween(f, A, B)1013  requires ha : ¬a ∈ A1014  requires hb : ¬b ∈ B1015  shows BijectiveBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))1016proof1017  constructor1018  . have oldInjective := Bijective.injective with hf1019    exact adjoinMap.injective with oldInjective, ha, hb1020  . have oldSurjective := Bijective.surjective with hf1021    exact adjoinMap.surjective with oldSurjective, ha10221023-- Injectivity from cancellation on values.1024theorem Injective.of_pointwise (f A B : Set)1025  requires function : f : A → B1026  requires cancel : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → x = y1027  shows InjectiveBetween(f, A, B)1028proof1029  unfold InjectiveBetween1030  refine ⟨function, ?_⟩1031  intros x hx y hy z hz relatesX relatesY1032  have valueX := FunctionBetween.apply_value with function, hx, relatesX1033  have valueY := FunctionBetween.apply_value with function, hy, relatesY1034  have same : f(x) = f(y)1035    rw [valueX, valueY]1036    rfl1037  exact cancel with x, hx, y, hy, same1038