Sets

Set-theory examples

Open in Workbench View on GitHub

1-- Set-theory examples2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67-- Primitive logical reasoning over sets.89-- Closed propositions evaluate by producing a checked proof.10eval 1 in {1, 2}1112theorem pair.left (x y : Set)13  shows x in pair(x, y)14proof15  have membership := pair.membership at x, y, x16  apply membership.backward17  left18  reflexivity1920theorem pair.right (x y : Set)21  shows y ∈ pair(x, y)22proof23  simp2425theorem equality.or_example (x y : Set)26  shows x = x or x = y27proof28  simp2930theorem equality.and_example (x : Set)31  shows x = x and x = x32proof33  simp3435theorem equality.exists_self (x : Set)36  shows exists y, y = x37proof38  simp3940theorem membership.identity (x y : Set)41  requires x in y42  shows x in y43proof44  simp4546theorem epsilon0.less.unfold (a b : Set)47  shows relates(epsilon0.less, a, b) <-> a in epsilon0 and b in epsilon0 and a in b48proof49  simp50