Function

Abstract

Licensed Foundation.Vorspiel.Function source for the concrete first-order pair extension.

Source-command excerpt selected from Foundation.Vorspiel.Function, lines 1-18, at Foundation revision 30a16ffa93d79d73ab4d02427fa00f50e039bf29. Only commands with live proof or source-elaboration consumers for the Kuratowski pair extension are retained.

The Lean file retains selected upstream commands and their compiler companions. The immutable source map, modification notices, full Apache-2.0 license and retirement condition are in Library/ConceptDynamics/foundation2026firstorder.md.

The retained commands supply the formulas, rewriting operations, set operations or proof and elaboration machinery used by the concrete pair interpretation. This excerpt does not represent the full upstream module.