FiniteCountableComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Countable joins bounded by a finite orthogonal target.

theorem OAI.BoundedHochschild.KadisonRingrose.countable_join_subequivalence line 22

Source documentation

Countably many projections, each embeddable into mutually orthogonal subprojections of a finite projection, have a join embeddable there.

theorem countable_join_subequivalence (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {Q : M} (hQ : IsStarProjection Q) (hfinite : FiniteCorner Q)
    (p q : ℕ → M) (hp : ∀ n, IsStarProjection (p n))
    (hq : ∀ n, IsStarProjection (q n))
    (horth : ∀ i j, i ≠ j → q i * q j = 0) (hqQ : ∀ n, q n ≤ Q)
    (hembed : ∀ n, ∃ v : PartialIso M, v.initial = p n ∧ v.final ≤ q n) :
    ∃ v : PartialIso M, v.final ≤ Q ∧ (∀ n, p n ≤ v.initial) ∧
      ∀ r : M, IsStarProjection r → (∀ n, p n ≤ r) → v.initial ≤ r := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteCorner