Grace/Cumulus/Set/Function/Image.g17

Open in Workbench Download source

Imports

Function · Algebra

Declarations

Source

1-- Images and preimages of functions and their algebra2-- 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.Function.Image8import Function9import Algebra1011-- The preimage of Y under a function with domain A.12def functionPreimage (f A Y : Set) : Set := { x ∈ A | f(x) ∈ Y }1314theorem functionPreimage.subset (f A Y : Set)15  shows functionPreimage(f, A, Y) ⊆ A16proof17  intros x hx18  simp [functionPreimage.membership] at hx19  exact hx.left2021theorem functionPreimage.of_apply (f A Y x : Set)22  requires hx : x ∈ A23  requires value : f(x) ∈ Y24  shows x ∈ functionPreimage(f, A, Y)25proof26  simp [functionPreimage.membership]2728-- Images2930theorem functionImage.empty (f B : Set)31  shows functionImage(f, ∅, B) = ∅32proof33  ext y34  constructor35  . intro hy36    simp [functionImage.membership] at hy37  . intro hy38    exfalso39    simpa using hy4041theorem functionImage.monotone (f A B S T : Set)42  requires h : S ⊆ T43  shows functionImage(f, S, B) ⊆ functionImage(f, T, B)44proof45  intros y hy46  simp [functionImage.membership] at hy47  obtain ⟨inB, x, hx, shape⟩ := hy48  simp [functionImage.membership]49  constructor50  . exact inB51  . refine ⟨x, (h with x, hx), shape⟩5253theorem functionImage.union2 (f A B S T : Set)54  shows functionImage(f, S ∪ T, B) = functionImage(f, S, B) ∪ functionImage(f, T, B)55proof56  ext y57  constructor58  . intro hy59    simp [functionImage.membership] at hy60    obtain ⟨inB, x, hx, shape⟩ := hy61    simp [union2.membership] at hx62    simp [union2.membership]63    cases hx with hS | hT64    . left65      simp [functionImage.membership]66      exact ⟨inB, x, hS, shape⟩67    . right68      simp [functionImage.membership]69      exact ⟨inB, x, hT, shape⟩70  . intro hy71    simp [union2.membership] at hy72    cases hy with hS | hT73    . exact functionImage.monotone at f, A, B, S, S ∪ T with (union2.subset_left at S, T), y, hS74    . exact functionImage.monotone at f, A, B, T, S ∪ T with (union2.subset_right at S, T), y, hT7576theorem functionImage.intersection_subset (f A B S T : Set)77  shows functionImage(f, S ∩ T, B) ⊆ functionImage(f, S, B) ∩ functionImage(f, T, B)78proof79  apply Subset.intersection_iff.backward80  constructor81  . exact functionImage.monotone at f, A, B, S ∩ T, S with (intersection.subset_left at S, T)82  . exact functionImage.monotone at f, A, B, S ∩ T, T with (intersection.subset_right at S, T)8384theorem Injective.apply_cancel (f A B x y : Set)85  requires injective : InjectiveBetween(f, A, B)86  requires hx : x ∈ A87  requires hy : y ∈ A88  requires same : f(x) = f(y)89  shows x = y90proof91  have function := injective.left92  have valueB := FunctionBetween.apply_closed with function, hx93  have hxz := FunctionBetween.relates_apply with function, hx94  have hyz := FunctionBetween.relates_apply with function, hy95  rw ← same at hyz96  exact Injective.cancel with injective, hx, hy, valueB, hxz, hyz9798theorem functionImage.intersection_of_injective (f A B S T : Set)99  requires injective : InjectiveBetween(f, A, B)100  requires hS : S ⊆ A101  requires hT : T ⊆ A102  shows functionImage(f, S ∩ T, B) = functionImage(f, S, B) ∩ functionImage(f, T, B)103proof104  apply Subset.antisymmetric105  . exact functionImage.intersection_subset at f, A, B, S, T106  . intros y hy107    simp [intersection.membership] at hy108    obtain ⟨inS, inT⟩ := hy109    simp [functionImage.membership] at inS110    simp [functionImage.membership] at inT111    obtain ⟨inB, x, hx, shapeX⟩ := inS112    obtain ⟨inB2, z, hz, shapeZ⟩ := inT113    have hxA : x ∈ A := hS with x, hx114    have hzA : z ∈ A := hT with z, hz115    have agree : f(x) = f(z)116      rw [← shapeX, ← shapeZ]117      rfl118    have same := Injective.apply_cancel with injective, hxA, hzA, agree119    simp [functionImage.membership]120    constructor121    . exact inB122    . witness x123      constructor124      . simp [intersection.membership]125      . exact shapeX126127theorem functionImage.difference_subset (f A B S T : Set)128  shows functionImage(f, S, B) ∖ functionImage(f, T, B) ⊆ functionImage(f, S ∖ T, B)129proof130  intros y hy131  simp [difference.membership] at hy132  obtain ⟨inS, notT⟩ := hy133  simp [functionImage.membership] at inS134  obtain ⟨inB, x, hx, shape⟩ := inS135  simp [functionImage.membership]136  constructor137  . exact inB138  . witness x139    constructor140    . simp [difference.membership]141      constructor142      . exact hx143      . intro inT144        apply notT145        simp [functionImage.membership]146        exact ⟨inB, x, inT, shape⟩147    . exact shape148149theorem functionImage.subset_iff (f A B S Y : Set)150  shows functionImage(f, S, B) ⊆ Y ↔ ∀ x ∈ S, f(x) ∈ B → f(x) ∈ Y151proof152  constructor153  . intros h x hx valueB154    have member : f(x) ∈ functionImage(f, S, B) by simp [functionImage.membership]155    exact h with f(x), member156  . intros h y hy157    simp [functionImage.membership] at hy158    obtain ⟨inB, x, hx, shape⟩ := hy159    rw shape160    rw shape at inB161    exact h with x, hx, inB162163-- Preimages164165theorem functionPreimage.empty (f A : Set)166  shows functionPreimage(f, A, ∅) = ∅167proof168  ext x169  simp [functionPreimage.membership]170171theorem functionPreimage.codomain (f A B : Set)172  requires function : f : A → B173  shows functionPreimage(f, A, B) = A174proof175  ext x176  constructor177  . intro hx178    exact functionPreimage.subset at f, A, B with x, hx179  . intro hx180    exact functionPreimage.of_apply with hx, (FunctionBetween.apply_closed with function, hx)181182theorem functionPreimage.monotone (f A Y Z : Set)183  requires h : Y ⊆ Z184  shows functionPreimage(f, A, Y) ⊆ functionPreimage(f, A, Z)185proof186  intros x hx187  simp [functionPreimage.membership] at hx188  simp [functionPreimage.membership]189190theorem functionPreimage.union2 (f A Y Z : Set)191  shows functionPreimage(f, A, Y ∪ Z) = functionPreimage(f, A, Y) ∪ functionPreimage(f, A, Z)192proof193  ext x194  simp [functionPreimage.membership, union2.membership]195196theorem functionPreimage.intersection (f A Y Z : Set)197  shows functionPreimage(f, A, Y ∩ Z) = functionPreimage(f, A, Y) ∩ functionPreimage(f, A, Z)198proof199  ext x200  simp [functionPreimage.membership, intersection.membership]201202theorem functionPreimage.difference (f A Y Z : Set)203  shows functionPreimage(f, A, Y ∖ Z) = functionPreimage(f, A, Y) ∖ functionPreimage(f, A, Z)204proof205  ext x206  simp [functionPreimage.membership, difference.membership]207208theorem functionPreimage.complement (f A B Y : Set)209  requires function : f : A → B210  shows functionPreimage(f, A, B ∖ Y) = A ∖ functionPreimage(f, A, Y)211proof212  have whole := functionPreimage.codomain with function213  rw [functionPreimage.difference, whole]214  rfl215216-- Images and preimages together217218theorem functionImage.preimage_subset (f A B Y : Set)219  shows functionImage(f, functionPreimage(f, A, Y), B) ⊆ Y220proof221  intros y hy222  simp [functionImage.membership] at hy223  obtain ⟨inB, x, hx, shape⟩ := hy224  simp [functionPreimage.membership] at hx225  rw shape226  exact hx.right227228theorem functionImage.preimage_of_subset (f A B Y : Set)229  requires function : f : A → B230  requires h : Y ⊆ functionImage(f, A, B)231  shows functionImage(f, functionPreimage(f, A, Y), B) = Y232proof233  apply Subset.antisymmetric234  . exact functionImage.preimage_subset at f, A, B, Y235  . intros y hy236    have inImage : y ∈ functionImage(f, A, B) := h with y, hy237    simp [functionImage.membership] at inImage238    obtain ⟨inB, x, hx, shape⟩ := inImage239    simp [functionImage.membership]240    constructor241    . exact inB242    . witness x243      constructor244      . simp [functionPreimage.membership]245      . exact shape246247theorem functionPreimage.image_superset (f A B S : Set)248  requires function : f : A → B249  requires hS : S ⊆ A250  shows S ⊆ functionPreimage(f, A, functionImage(f, S, B))251proof252  intros x hx253  simp [functionPreimage.membership]254  constructor255  . exact hS with x, hx256  . have value := FunctionBetween.apply_closed with function, (hS with x, hx)257    simp [functionImage.membership]258259theorem functionPreimage.image_of_injective (f A B S : Set)260  requires injective : InjectiveBetween(f, A, B)261  requires hS : S ⊆ A262  shows functionPreimage(f, A, functionImage(f, S, B)) = S263proof264  have function := injective.left265  apply Subset.antisymmetric266  . intros x hx267    simp [functionPreimage.membership] at hx268    obtain ⟨hxA, inImage⟩ := hx269    simp [functionImage.membership] at inImage270    obtain ⟨inB, z, hz, shape⟩ := inImage271    have same := Injective.apply_cancel with injective, hxA, (hS with z, hz), shape272    rwa same273  . exact functionPreimage.image_superset with function, hS274275theorem functionImage.compose (g f A B C S : Set)276  requires fFunction : f : A → B277  requires gFunction : g : B → C278  requires hS : S ⊆ A279  shows functionImage(compose(g, f, A, B, C), S, C) = functionImage(g, functionImage(f, S, B), C)280proof281  have composed := compose.function with fFunction, gFunction282  ext y283  constructor284  . intro hy285    simp [functionImage.membership] at hy286    obtain ⟨inC, x, hx, shape⟩ := hy287    have hxA : x ∈ A := hS with x, hx288    have step := compose.apply with fFunction, gFunction, hxA289    simp [functionImage.membership]290    constructor291    . exact inC292    . witness f(x)293      constructor294      . have value := FunctionBetween.apply_closed with fFunction, hxA295        simp [functionImage.membership]296        exact ⟨value, x, hx, rfl⟩297      . rw [shape, step]298        rfl299  . intro hy300    simp [functionImage.membership] at hy301    obtain ⟨inC, z, hz, shape⟩ := hy302    simp [functionImage.membership] at hz303    obtain ⟨inB, x, hx, shapeZ⟩ := hz304    have hxA : x ∈ A := hS with x, hx305    have step := compose.apply with fFunction, gFunction, hxA306    simp [functionImage.membership]307    constructor308    . exact inC309    . witness x310      constructor311      . exact hx312      . rw [shape, shapeZ, step]313        rfl314315theorem functionPreimage.compose (g f A B C Z : Set)316  requires fFunction : f : A → B317  requires gFunction : g : B → C318  shows functionPreimage(compose(g, f, A, B, C), A, Z) = functionPreimage(f, A, functionPreimage(g, B, Z))319proof320  ext x321  constructor322  . intro hx323    simp [functionPreimage.membership] at hx324    obtain ⟨hxA, value⟩ := hx325    have step := compose.apply with fFunction, gFunction, hxA326    rw step at value327    have inB := FunctionBetween.apply_closed with fFunction, hxA328    simp [functionPreimage.membership]329  . intro hx330    simp [functionPreimage.membership] at hx331    obtain ⟨hxA, inner⟩ := hx332    simp [functionPreimage.membership] at inner333    have step := compose.apply with fFunction, gFunction, hxA334    simp [functionPreimage.membership]335336theorem functionImage.identity_of_subset (A S : Set)337  requires hS : S ⊆ A338  shows functionImage(identity(A), S, A) = S339proof340  ext y341  constructor342  . intro hy343    simp [functionImage.membership] at hy344    obtain ⟨inA, x, hx, shape⟩ := hy345    have fixed := identity.apply with (hS with x, hx)346    rwa [shape, fixed]347  . intro hy348    simp [functionImage.membership]349    constructor350    . exact hS with y, hy351    . witness y352      constructor353      . exact hy354      . symm355        exact identity.apply with (hS with y, hy)356357-- An injection is a bijection onto its image.358theorem Injective.corestrict (f A B : Set)359  requires injective : InjectiveBetween(f, A, B)360  shows InjectiveBetween(f, A, functionImage(f, A, B))361proof362  have function := Injective.function with injective363  constructor364  . exact functionImage.corestrict with function365  . intros x hx y hy z hz hxz hyz366    have hzB := functionImage.subset at f, A, B with z, hz367    exact injective.right with x, hx, y, hy, z, hzB, hxz, hyz368369-- Restricting an injection keeps it injective, with the same image.370theorem restrict.injective (f A B S : Set)371  requires injective : InjectiveBetween(f, A, B)372  requires subset : S ⊆ A373  shows InjectiveBetween(restrict(f, S), S, B)374proof375  have function := Injective.function with injective376  have closed : ∀ x ∈ S, f(x) ∈ B377    intros x hx378    exact FunctionBetween.apply_closed with function, (subset with x, hx)379  have restricted := restrict.function with function, subset, closed380  constructor381  . exact restricted382  . intros x hx y hy z hz hxz hyz383    have valueX := FunctionBetween.apply_value with restricted, hx, hxz384    have valueY := FunctionBetween.apply_value with restricted, hy, hyz385    have stepX := restrict.apply with function, subset, closed, hx386    have stepY := restrict.apply with function, subset, closed, hy387    have same : f(x) = f(y) by cc388    exact Injective.apply_cancel with injective, (subset with x, hx), (subset with y, hy), same389390theorem functionImage.restrict (f A B S : Set)391  requires function : f : A → B392  requires subset : S ⊆ A393  shows functionImage(restrict(f, S), S, B) = functionImage(f, S, B)394proof395  have closed : ∀ x ∈ S, f(x) ∈ B396    intros x hx397    exact FunctionBetween.apply_closed with function, (subset with x, hx)398  ext y399  constructor400  . intro hy401    simp [functionImage.membership] at hy402    obtain ⟨inB, x, hx, shape⟩ := hy403    have step := restrict.apply with function, subset, closed, hx404    rw step at shape405    simp [functionImage.membership]406    constructor407    . exact inB408    . refine ⟨x, hx, shape⟩409  . intro hy410    simp [functionImage.membership] at hy411    obtain ⟨inB, x, hx, shape⟩ := hy412    have step := restrict.apply with function, subset, closed, hx413    rw ← step at shape414    simp [functionImage.membership]415    constructor416    . exact inB417    . refine ⟨x, hx, shape⟩418419theorem functionImage.insert (f A B x S : Set)420  requires function : f : A → B421  requires hx : x ∈ A422  shows functionImage(f, insert(x, S), B) = insert(f(x), functionImage(f, S, B))423proof424  have value := FunctionBetween.apply_closed with function, hx425  ext y426  constructor427  . intro hy428    simp [functionImage.membership] at hy429    obtain ⟨inB, z, hz, shape⟩ := hy430    have split := insert.membership.forward with hz431    apply insert.membership.backward432    cases split with same | inS433    . left434      rw [shape, same]435      rfl436    . right437      simp [functionImage.membership]438      constructor439      . exact inB440      . refine ⟨z, inS, shape⟩441  . intro hy442    have split := insert.membership.forward with hy443    cases split with same | inImage444    . have inserted : x ∈ insert(x, S)445        apply insert.membership.backward446        left447        rfl448      rw same449      simp [functionImage.membership]450      constructor451      . exact value452      . witness x453        constructor454        . exact inserted455        . rfl456    . simp [functionImage.membership] at inImage457      obtain ⟨inB, z, hz, shape⟩ := inImage458      have inserted : z ∈ insert(x, S)459        apply insert.membership.backward460        right461        exact hz462      simp [functionImage.membership]463      constructor464      . exact inB465      . refine ⟨z, inserted, shape⟩466