-- The set of all functions from A to B
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Set.Function.Space
import Image
import Powerset

-- Every function from A to B is a subset of A × B, so the functions form
-- a set carved out of the power set.
def functionSpace (A B : Set) : Set := { f ∈ 𝒫(A × B) | FunctionBetween(f, A, B) }

theorem functionSpace.mem_iff (f A B : Set)
  shows f ∈ functionSpace(A, B) ↔ FunctionBetween(f, A, B)
proof
  constructor
  . intro h
    simp [functionSpace] at h
    exact h.right
  . intro h
    have included : f ⊆ A × B := h.left
    have bounded : f ∈ 𝒫(A × B) := powerset.membership_iff.backward with included
    simp [functionSpace]

theorem functionSpace.subset_powerset (A B : Set)
  shows functionSpace(A, B) ⊆ 𝒫(A × B)
proof
  intros f hf
  simp [functionSpace] at hf
  exact hf.left

theorem functionSpace.identity (A : Set)
  shows identity(A) ∈ functionSpace(A, A)
proof
  exact functionSpace.mem_iff.backward with (identity.function at A)

theorem functionSpace.constant (A B y : Set)
  requires hy : y ∈ B
  shows constantFunction(A, B, y) ∈ functionSpace(A, B)
proof
  have function := constantFunction.function at A, B, y with hy
  exact functionSpace.mem_iff.backward with function

theorem functionSpace.compose (f g A B C : Set)
  requires hf : f ∈ functionSpace(A, B)
  requires hg : g ∈ functionSpace(B, C)
  shows compose(g, f, A, B, C) ∈ functionSpace(A, C)
proof
  have fFunction := functionSpace.mem_iff.forward with hf
  have gFunction := functionSpace.mem_iff.forward with hg
  have composed := compose.function with fFunction, gFunction
  exact functionSpace.mem_iff.backward with composed

theorem functionSpace.monotone (A B C : Set)
  requires h : B ⊆ C
  shows functionSpace(A, B) ⊆ functionSpace(A, C)
proof
  intros f hf
  have function := functionSpace.mem_iff.forward with hf
  have widened := FunctionBetween.codomain_of_values at f, A, B, C with function
  apply functionSpace.mem_iff.backward
  apply widened
  intros x hx
  exact h with f(x), (FunctionBetween.apply_closed with function, hx)

theorem functionSpace.empty_codomain (A : Set)
  requires nonempty : Nonempty(A)
  shows functionSpace(A, ∅) = ∅
proof
  apply Subset.empty_iff.forward
  intros f hf
  have function := functionSpace.mem_iff.forward with hf
  obtain ⟨x, hx⟩ := nonempty
  have value := FunctionBetween.apply_closed with function, hx
  exfalso
  exact set.empty with value

theorem functionSpace.empty_domain (B : Set)
  shows functionSpace(∅, B) = {∅}
proof
  ext f
  constructor
  . intro hf
    have function := functionSpace.mem_iff.forward with hf
    have included : f ⊆ ∅ × B := function.left
    have emptyProduct := product.left_empty at B
    rw emptyProduct at included
    have empty := Subset.empty_iff.forward with included
    rw empty
    exact singleton.self
  . intro hf
    simp [singleton.membership] at hf
    rw hf
    exact functionSpace.mem_iff.backward with (FunctionBetween.empty at B)

-- A constant function shows that the functions into a nonempty set exist.
theorem functionSpace.nonempty (A B : Set)
  requires inhabited : Nonempty(B)
  shows Nonempty(functionSpace(A, B))
proof
  obtain ⟨y, hy⟩ := inhabited
  have function := constantFunction.function at A, B, y with hy
  have member := functionSpace.mem_iff.backward with function
  exact ⟨constantFunction(A, B, y), member⟩