Grace/Cumulus/Set/Classes.g17

Open in Workbench Download source

Imports

Basic

Declarations

• Universe class
• Natural class
• MemberOf class
• SubsetsOf class
• Inhabited class
• naturalsIn def
• Natural.of_Nat theorem derivation
• Universe.membership theorem derivation
• MemberOf.characterization theorem derivation
• SubsetsOf.characterization theorem derivation
• SubsetsOf.Universe theorem derivation

Source

1-- Classes and proper classes2-- 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.Classes8import Basic910namespace Class1112class Universe (x : Set) := { x | x = x }13class Natural (x : Set) := Nat(x)14class MemberOf (x A : Set) := x ∈ A15class SubsetsOf (A : Class) := { X : Set | ∀ x ∈ X, x ∈ A }16class Inhabited (A : Set) := ∃ x, x ∈ A1718def naturalsIn (A : Set) : Set := { x ∈ A | x ∈ Natural }1920theorem Natural.of_Nat (n : Nat)21  shows n ∈ Natural22proof23  simp [Natural]2425theorem Universe.membership (x : Set)26  shows x ∈ Universe ↔ x = x27proof28  simp [Universe]2930theorem MemberOf.characterization (x A : Set)31  shows x ∈ MemberOf(A) ↔ x ∈ A32proof33  simp [MemberOf]3435theorem SubsetsOf.characterization (X A : Set)36  shows X ∈ SubsetsOf(A) ↔ (X ⊆ A)37proof38  simp3940theorem SubsetsOf.Universe41  shows SubsetsOf(Universe) = Universe42proof43  simp4445end Class4647export open Grace.Cumulus.Set.Classes.Class48