BFPP.lean

1import BFPP.Transfer2import BFPP.Suprema3import BFPP.BoundedFamilies4import BFPP.Envelopes5import BFPP.Profiles6import BFPP.ProfileGeometry7import BFPP.Center8import BFPP.TwoProfiles9import BFPP.TwoProfileGeometry10import BFPP.ContinuousBall11import BFPP.FSpaceNecessary12import BFPP.Deficits13import BFPP.Analysis14import BFPP.Regularization15import BFPP.C0Profiles16import BFPP.FiniteSynthesis17import BFPP.StepFunctions18import BFPP.StepAlgebra19import BFPP.PositiveSynthesis20import BFPP.CenteredSynthesis21import BFPP.Families22import BFPP.Realization23import BFPP.OrdinalIndex24import BFPP.Cozero25import BFPP.SaturatedChains26import BFPP.SignExtension27import BFPP.Hartogs28import BFPP.SignRecursion29import BFPP.SignTermination30import BFPP.SignRealization31import BFPP.ChainCompleteness32import BFPP.BooleanGap33import BFPP.CofinalSequences34import BFPP.IndexedGaps35import BFPP.ClopenCompleteness36import BFPP.ClopenPairs37import BFPP.CofinalReindexing38import BFPP.Necessity39import BFPP.EDSupremum40import BFPP.BallOrderGeometry41import BFPP.InvariantIntervals42import BFPP.LatticeFixedPoint43import BFPP.Characterization44import BFPP.OrdinalCofinality45import BFPP.CountablePairs46import BFPP.RegularPairs47import BFPP.OrdinalPairs48import BFPP.ProfileExtension49import BFPP.ExtensionDelay50import BFPP.Interleaving51import BFPP.TwoProfileStructure52import BFPP.EncodedDomain53import BFPP.EnvelopeOrder54import BFPP.InterleavingEnvelopes55import BFPP.ProfileRestriction56import BFPP.EncodedMaps57import BFPP.PrefixFactorization58import BFPP.TransfinitePropagator59import BFPP.DelayPrefixBound60import BFPP.EncodedRecurrence61import BFPP.MainTransfinite62import BFPP.EncodedRules63import BFPP.ComplexBall64import BFPP.SynthesisMeasure65import BFPP.SynthesisIntegral66import BFPP.PointwiseSupremum67import BFPP.PointwisePrefixes68import BFPP.TerminalSupremum69import BFPP.TerminalNormalization70import BFPP.NormalizedAppendix71import BFPP.ConvexIntegral72import BFPP.BallScaling73import BFPP.DiscretePropagation

SHA-256