TheoremSections

Shared theorem context, nested scope, and application outside a section

Open in Workbench View on GitHub

1-- Shared theorem context, nested scope, and application outside a section.2-- 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 TheoremSections8namespace SectionExamples9import Grace.Cumulus.Set1011section Membership12variable (A x : Set)13hypothesis hx : x ∈ A1415theorem member16  shows x ∈ A17proof18  simp1920section Pair21variable (y : Set)22hypothesis hy : y ∈ A2324theorem both25  shows x ∈ A ∧ y ∈ A26proof27  simp28end Pair2930theorem member_again31  shows x ∈ A32proof33  simp34end Membership3536-- The exported theorem takes the former section context as arguments.37theorem use_both (B a b : Set)38  requires ha : a ∈ B39  requires hb : b ∈ B40  shows a ∈ B ∧ b ∈ B41proof42  simp4344end SectionExamples45