Grace/Cumulus/Set/Inclusion.g17

Open in Workbench Download source

Imports

Function

Declarations

Source

1-- The canonical inclusion graph of a subset2-- 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.Inclusion8import Function910-- Its codomain can be larger than its domain. The only mathematical11-- obligation is the stated inclusion; graph and application laws are derived.12defgraph inclusionMap (A B : Set) (x ∈ A) : B := x13requires subset : A ⊆ B14proof15  unfold Subset at subset16  exact subset with x, member17