InfinitePairChains.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Increasing chains of pairs implementing properly infinite projections.

def OAI.BoundedHochschild.KadisonRingrose.IsInfinitePair line 19
Source documentation
Two embeddings of a common projection into orthogonal subprojections.
```
def IsInfinitePair (a : PartialIso M × PartialIso M) : Prop :=
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.infinitePair_cross_orthogonal line 23

theorem OAI.BoundedHochschild.KadisonRingrose.infinitePair_chain_upper line 39

Source documentation

The pair order preserves both common initial supports and orthogonality at a chain supremum.

theorem infinitePair_chain_upper (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (C : Set (PartialIso M × PartialIso M)) (hC : ∀ a ∈ C, IsInfinitePair a)
    (hchain : IsChain (· ≤ ·) C) (hne : C.Nonempty) :
    ∃ a : PartialIso M × PartialIso M, IsInfinitePair a ∧ ∀ b ∈ C, b ≤ a := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.IsInfinitePair