Grace/Cumulus/Set/Function/Space.g17

Open in Workbench Download source

Imports

Image · Powerset

Declarations

Source

1-- The set of all functions from A to B2-- 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.Space8import Image9import Powerset1011-- Every function from A to B is a subset of A × B, so the functions form12-- a set carved out of the power set.13def functionSpace (A B : Set) : Set := { f ∈ 𝒫(A × B) | FunctionBetween(f, A, B) }1415theorem functionSpace.mem_iff (f A B : Set)16  shows f ∈ functionSpace(A, B) ↔ FunctionBetween(f, A, B)17proof18  constructor19  . intro h20    simp [functionSpace] at h21    exact h.right22  . intro h23    have included : f ⊆ A × B := h.left24    have bounded : f ∈ 𝒫(A × B) := powerset.membership_iff.backward with included25    simp [functionSpace]2627theorem functionSpace.subset_powerset (A B : Set)28  shows functionSpace(A, B) ⊆ 𝒫(A × B)29proof30  intros f hf31  simp [functionSpace] at hf32  exact hf.left3334theorem functionSpace.identity (A : Set)35  shows identity(A) ∈ functionSpace(A, A)36proof37  exact functionSpace.mem_iff.backward with (identity.function at A)3839theorem functionSpace.constant (A B y : Set)40  requires hy : y ∈ B41  shows constantFunction(A, B, y) ∈ functionSpace(A, B)42proof43  have function := constantFunction.function at A, B, y with hy44  exact functionSpace.mem_iff.backward with function4546theorem functionSpace.compose (f g A B C : Set)47  requires hf : f ∈ functionSpace(A, B)48  requires hg : g ∈ functionSpace(B, C)49  shows compose(g, f, A, B, C) ∈ functionSpace(A, C)50proof51  have fFunction := functionSpace.mem_iff.forward with hf52  have gFunction := functionSpace.mem_iff.forward with hg53  have composed := compose.function with fFunction, gFunction54  exact functionSpace.mem_iff.backward with composed5556theorem functionSpace.monotone (A B C : Set)57  requires h : B ⊆ C58  shows functionSpace(A, B) ⊆ functionSpace(A, C)59proof60  intros f hf61  have function := functionSpace.mem_iff.forward with hf62  have widened := FunctionBetween.codomain_of_values at f, A, B, C with function63  apply functionSpace.mem_iff.backward64  apply widened65  intros x hx66  exact h with f(x), (FunctionBetween.apply_closed with function, hx)6768theorem functionSpace.empty_codomain (A : Set)69  requires nonempty : Nonempty(A)70  shows functionSpace(A, ∅) = ∅71proof72  apply Subset.empty_iff.forward73  intros f hf74  have function := functionSpace.mem_iff.forward with hf75  obtain ⟨x, hx⟩ := nonempty76  have value := FunctionBetween.apply_closed with function, hx77  exfalso78  exact set.empty with value7980theorem functionSpace.empty_domain (B : Set)81  shows functionSpace(∅, B) = {∅}82proof83  ext f84  constructor85  . intro hf86    have function := functionSpace.mem_iff.forward with hf87    have included : f ⊆ ∅ × B := function.left88    have emptyProduct := product.left_empty at B89    rw emptyProduct at included90    have empty := Subset.empty_iff.forward with included91    rw empty92    exact singleton.self93  . intro hf94    simp [singleton.membership] at hf95    rw hf96    exact functionSpace.mem_iff.backward with (FunctionBetween.empty at B)9798-- A constant function shows that the functions into a nonempty set exist.99theorem functionSpace.nonempty (A B : Set)100  requires inhabited : Nonempty(B)101  shows Nonempty(functionSpace(A, B))102proof103  obtain ⟨y, hy⟩ := inhabited104  have function := constantFunction.function at A, B, y with hy105  have member := functionSpace.mem_iff.backward with function106  exact ⟨constantFunction(A, B, y), member⟩107