OAI/Analysis/KadisonKastler/StateInputsStability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Universal strong stability from state homogeneity and bicentralizers

  1. theorem OAI.KadisonKastler.universal_strong_stability_of_state_inputs line 16

    Source documentation

    State homogeneity and Powers absorption for bicentralizers imply universal strong stability.

    theorem universal_strong_stability_of_state_inputs
    (hhom : PublishedTypeIII1StateHomogeneity.{u})
    (hbic : PublishedPowersAbsorptionBicentralizer.{u}) : UniversalStrongStability.{u} :=
…