OAI/Analysis/KadisonKastler/StabilityStatement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Universal strong Kadison–Kastler stability

The tolerance in Theorem 1.1 of Universal strong Kadison–Kastler stability is chosen before the Hilbert space and the represented von Neumann algebras.

  1. def OAI.KadisonKastler.UniversalStrongStability line 17

    Source documentation

    Universal strong stability, at an arbitrary fixed universe level.

    Also declared: ComparatorChallenges/StrongKadisonKastler.lean:31 (same declaration text).

    def UniversalStrongStability : Prop :=
…