ExhaustionWeakEquivalence.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

Every realization point has unique nondegenerate interior coordinates

theorem OAI.Thomason.Construction.RealizationPrism.normalizeSimplex_fullSupport line 22
theorem OAI.Thomason.Construction.RealizationPrism.normalizeSupported_fullSupport line 30
theorem OAI.Thomason.Construction.RealizationPrism.normalization_fullSupport line 37
Source documentation
No coordinate of the intrinsic nondegenerate representative vanishes.
```
theorem normalization_fullSupport (K : SSet.{0}) (x : SSet.toTop.obj K) :
    (normalization K x).2 ∈ fullSupport (normalization K x).1.dim := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.normalization, OAI.Thomason.Construction.RealizationPrism.fullSupport
def OAI.Thomason.Construction.RealizationPrism.interiorCoordinatesEquiv line 45
Source documentation
The underlying set of a realization is the disjoint union of nondegenerate simplex interiors. This does not give the disjoint-union topology.
```
def interiorCoordinatesEquiv (K : SSet.{0}) :
    SSet.toTop.obj K ≃ Σ s : K.N, fullSupport s.dim where
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.fullSupport
theorem OAI.Thomason.Construction.RealizationPrism.standard_boundary_carrier_iff line 80
Source documentation
A supported simplex of the standard simplex belongs to its boundary precisely when some original barycentric coordinate vanishes.
```
theorem standard_boundary_carrier_iff (n : ℕ) (x : StdSimplex ℝ (Fin (n+1))) :
    simplexCarrier (Δ[n] : SSet.{0}) (SSet.yonedaEquiv (𝟙 _)) x ≤ SSet.boundary n ↔
      ∃ i, x.weights i = 0 := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.simplexCarrier

theorem OAI.Thomason.Construction.RealizationPrism.standard_boundary_point_iff line 105

Source documentation

The actual realized boundary has exactly the familiar zero-coordinate locus.

theorem standard_boundary_point_iff (n : ℕ) (x : StdSimplex ℝ (Fin (n+1))) :
    simplexPoint (Δ[n] : SSet.{0}) (SSet.yonedaEquiv (𝟙 _)) x ∈
        Set.range (SSet.toTop.map (SSet.boundary n).ι).hom ↔
      ∃ i, x.weights i = 0 := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint

theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_standard_id line 130
Source documentation
The parameter map of the identity simplex is the inverse of the standard realization homeomorphism.
```
theorem simplexPoint_standard_id (n : ℕ) (x : StdSimplex ℝ (Fin (n+1))) :
    simplexPoint (Δ[n] : SSet.{0}) (SSet.yonedaEquiv (𝟙 _)) x =
      (SimplexCategory.mk n).toTopHomeo.symm x := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.simplexPoint
def OAI.Thomason.Construction.RealizationPrism.boundaryLocus line 143
Source documentation
The boundary locus, including the empty boundary in dimension zero.
```
def boundaryLocus (n : ℕ) : Set (StdSimplex ℝ (Fin (n+1))) :=
…
```
def OAI.Thomason.Construction.RealizationPrism.boundaryCoordinates line 147
Source documentation
The barycentric coordinates of the actual boundary inclusion.
```
def boundaryCoordinates (n : ℕ) :
    C(SSet.toTop.obj (SSet.boundary n : SSet.{0}), StdSimplex ℝ (Fin (n+1))) :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.boundaryCoordinates_isClosedEmbedding line 152
theorem OAI.Thomason.Construction.RealizationPrism.range_boundaryCoordinates line 157
def OAI.Thomason.Construction.RealizationPrism.boundaryHomeomorph line 177
Source documentation
The actual boundary realization is homeomorphic to the zero-coordinate locus of the barycentric simplex.
```
def boundaryHomeomorph (n : ℕ) :
    SSet.toTop.obj (SSet.boundary n : SSet.{0}) ≃ₜ boundaryLocus n :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryLocus
theorem OAI.Thomason.Construction.RealizationPrism.boundaryHomeomorph_inclusion line 184
Source documentation
The homeomorphism identifies the realized boundary arrow with the actual barycentric subspace inclusion, not just with an abstract homeomorphic pair.
```
theorem boundaryHomeomorph_inclusion (n : ℕ)
    (x : SSet.toTop.obj (SSet.boundary n : SSet.{0})) :
    (boundaryHomeomorph n x).val =
      (SimplexCategory.mk n).toTopHomeo
        ((SSet.toTop.map (SSet.boundary n).ι).hom x) := rfl
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryHomeomorph
def OAI.Thomason.Construction.RealizationPrism.boundaryInclusion line 213
Source documentation
The literal inclusion of the barycentric boundary subspace.
```
def boundaryInclusion (n : ℕ) :
    TopCat.of (boundaryLocus n) ⟶ TopCat.of (StdSimplex ℝ (Fin (n+1))) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryLocus
def OAI.Thomason.Construction.RealizationPrism.boundaryArrowIso line 218
Source documentation
The whole realized boundary arrow agrees with the barycentric pair.
```
def boundaryArrowIso (n : ℕ) :
    Arrow.mk (SSet.toTop.map (SSet.boundary n).ι) ≅ Arrow.mk (boundaryInclusion n) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion
theorem OAI.Thomason.Construction.RealizationPrism.singular_boundary_lifting_iff line 229
Source documentation
Singular boundary filling is exactly lifting against the actual barycentric boundary inclusion.
```
theorem singular_boundary_lifting_iff {X Y : TopCat.{0}} (p : X ⟶ Y) (n : ℕ) :
    HasLiftingProperty (SSet.boundary n).ι (TopCat.toSSet.map p) ↔
      HasLiftingProperty (boundaryInclusion n) p :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion
theorem OAI.Thomason.Construction.RealizationPrism.singular_boundary_rlp_iff line 237
Source documentation
The entire simplicial boundary lifting class has this concrete topological interpretation.
```
theorem singular_boundary_rlp_iff {X Y : TopCat.{0}} (p : X ⟶ Y) :
    I.rlp (TopCat.toSSet.map p) ↔ ∀ n, HasLiftingProperty (boundaryInclusion n) p := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion
theorem OAI.Thomason.Construction.RealizationPrism.singular_weak_of_boundary_lifting line 248
Source documentation
Maps lifting against every barycentric boundary induce actual weak homotopy equivalences of singular realizations.
```
theorem singular_weak_of_boundary_lifting {X Y : TopCat.{0}} (p : X ⟶ Y)
    (h : ∀ n, HasLiftingProperty (boundaryInclusion n) p) :
    realizationWeakEquivalences (TopCat.toSSet.map p) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.RealizationPrism.realization_mono_lifting line 256
Source documentation
Elementary barycentric boundary lifts extend over every realized simplicial monomorphism. This is the actual topological lifting property, obtained through the adjunction and the proved boundary generation theorem.
```
theorem realization_mono_lifting {X Y : TopCat.{0}} (p : X ⟶ Y)
    (h : ∀ n, HasLiftingProperty (boundaryInclusion n) p)
    {K L : SSet.{0}} (i : K ⟶ L) [Mono i] :
    HasLiftingProperty (SSet.toTop.map i) p := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion

def OAI.Thomason.Construction.RealizationPrism.relativeBoundaryExtension line 267

Source documentation

A concrete continuous extension preserving the prescribed map on a subcomplex and its image under p.

def relativeBoundaryExtension {X Y : TopCat.{0}} (p : X ⟶ Y)
    (h : ∀ n, HasLiftingProperty (boundaryInclusion n) p)
    (K : SSet.{0}) (A : K.Subcomplex)
    (a : SSet.toTop.obj (A : SSet) ⟶ X) (b : SSet.toTop.obj K ⟶ Y)
    (sq : CommSq a (SSet.toTop.map A.ι) p b) : SSet.toTop.obj K ⟶ X := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion

theorem OAI.Thomason.Construction.RealizationPrism.relativeBoundaryExtension_restrict line 276
theorem OAI.Thomason.Construction.RealizationPrism.relativeBoundaryExtension_comp line 286
theorem OAI.Thomason.Construction.RealizationPrism.simplexPoint_as_realized_map line 312
theorem OAI.Thomason.Construction.RealizationPrism.boundaryLocus_eq_compl_fullSupport line 321
def OAI.Thomason.Construction.RealizationPrism.cellBoundaryMap line 329
Source documentation
The actual attaching map is the realization of the simplicial boundary followed by the given characteristic simplex.
```
def cellBoundaryMap (K : SSet.{0}) {n : ℕ} (s : K.obj (.op (.mk n))) :
    SSet.toTop.obj (SSet.boundary n : SSet.{0}) ⟶ SSet.toTop.obj K :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.cellBoundaryMap_coordinates line 333
theorem OAI.Thomason.Construction.RealizationPrism.range_cellBoundaryMap line 346
theorem OAI.Thomason.Construction.RealizationPrism.cell_boundary_eq_closure_diff line 355
Source documentation
The boundary image is exactly the part of the closed characteristic cell outside its own interior, allowing arbitrary identifications of faces.
```
theorem cell_boundary_eq_closure_diff (K : SSet.{0}) (s : K.N) :
    Set.range (cellBoundaryMap K s.simplex).hom =
      closure (simplexPoint K s.simplex '' fullSupport s.dim) \
        (simplexPoint K s.simplex '' fullSupport s.dim) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.cellBoundaryMap, OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.RealizationPrism.fullSupport
theorem OAI.Thomason.Construction.RealizationPrism.carrier_interior line 392
Source documentation
An interior point has the whole characteristic simplex as its carrier.
```
theorem carrier_interior (K : SSet.{0}) {n : ℕ} (s : K.obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (n+1))) (hx : x ∈ fullSupport n) :
    carrier K (simplexPoint K s x) = SSet.Subcomplex.ofSimplex s := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.fullSupport, OAI.Thomason.Construction.RealizationPrism.carrier, OAI.Thomason.Construction.RealizationPrism.simplexPoint
theorem OAI.Thomason.Construction.RealizationPrism.interior_mem_subcomplex_iff line 409
Source documentation
A subcomplex contains a point of a simplex interior exactly when it contains the simplex itself.
```
theorem interior_mem_subcomplex_iff (K : SSet.{0}) (A : K.Subcomplex) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1))) (hx : x ∈ fullSupport n) :
    simplexPoint K s x ∈ Set.range (SSet.toTop.map A.ι).hom ↔ s ∈ A.obj _ := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.fullSupport, OAI.Thomason.Construction.RealizationPrism.simplexPoint
theorem OAI.Thomason.Construction.RealizationPrism.boundary_point_dimension_lt line 417
Source documentation
Boundary points of an n-simplex belong to cells of strictly smaller dimension, including when the original simplex or its faces are degenerate.
```
theorem boundary_point_dimension_lt (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n))) (x : StdSimplex ℝ (Fin (n+1))) (hx : x ∈ boundaryLocus n) :
    (normalization K (simplexPoint K s x)).1.dim < n := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryLocus, OAI.Thomason.Construction.RealizationPrism.normalization, OAI.Thomason.Construction.RealizationPrism.simplexPoint
theorem OAI.Thomason.Construction.RealizationPrism.cellBoundaryMap_dimension_lt line 428
Source documentation
The actual attaching map lands entirely in lower-dimensional cells.
```
theorem cellBoundaryMap_dimension_lt (K : SSet.{0}) {n : ℕ}
    (s : K.obj (.op (.mk n)))
    (x : SSet.toTop.obj (SSet.boundary n : SSet.{0})) :
    (normalization K ((cellBoundaryMap K s).hom x)).1.dim < n := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.normalization, OAI.Thomason.Construction.RealizationPrism.cellBoundaryMap
abbrev OAI.Thomason.Construction.RealizationPrism.simplicialBoundaryCell line 460
abbrev OAI.Thomason.Construction.RealizationPrism.realizedBoundaryCell line 462
abbrev OAI.Thomason.Construction.RealizationPrism.barycentricBoundaryCell line 464
def OAI.Thomason.Construction.RealizationPrism.realizeBoundaryAttachment line 468
Source documentation
Realization carries a simultaneous simplicial boundary attachment to the corresponding simultaneous topological attachment.
```
def realizeBoundaryAttachment {X Y : SSet.{0}} {n : ℕ} {f : X ⟶ Y}
    (c : AttachCells.{0} (simplicialBoundaryCell n) f) :
    AttachCells.{0} (realizedBoundaryCell n) (SSet.toTop.map f) where
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.simplicialBoundaryCell, OAI.Thomason.Construction.RealizationPrism.realizedBoundaryCell
def OAI.Thomason.Construction.RealizationPrism.realizedCellComplexOfMono line 490
Source documentation
The topological skeletal presentation with the original realized boundary arrows.
```
def realizedCellComplexOfMono {X Y : SSet.{0}} (i : X ⟶ Y) [Mono i] :
    RelativeCellComplex.{0} realizedBoundaryCell (SSet.toTop.map i) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.realizedBoundaryCell
def OAI.Thomason.Construction.RealizationPrism.barycentricCellComplexOfMono line 501
Source documentation
Every realized monomorphism is obtained by attaching actual barycentric n-simplices along their boundaries at stage n.
```
def barycentricCellComplexOfMono {X Y : SSet.{0}} (i : X ⟶ Y) [Mono i] :
    RelativeCellComplex.{0} barycentricBoundaryCell (SSet.toTop.map i) where
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.barycentricBoundaryCell
theorem OAI.Thomason.Construction.RealizationPrism.mem_range_iff_normalization line 527
Source documentation
Subcomplex membership can be tested on the unique nondegenerate interior representative of the point.
```
theorem mem_range_iff_normalization (K : SSet.{0}) (A : K.Subcomplex)
    (x : SSet.toTop.obj K) :
    x ∈ Set.range (SSet.toTop.map A.ι).hom ↔
      (normalization K x).1.simplex ∈ A.obj _ := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.normalization
theorem OAI.Thomason.Construction.RealizationPrism.range_iSup_inclusion line 540
Source documentation
Realization carries an arbitrary subcomplex union to the literal union of the corresponding topological subspaces.
```
theorem range_iSup_inclusion (K : SSet.{0}) {ι : Type} (A : ι → K.Subcomplex) :
    Set.range (SSet.toTop.map (iSup A).ι).hom =
      ⋃ i, Set.range (SSet.toTop.map (A i).ι).hom := by
…
```
theorem OAI.Thomason.Construction.RealizationPrism.range_realized_map line 550
Source documentation
The actual point-set image of a realized simplicial map is exactly the realization of its simplicial image subcomplex.
```
theorem range_realized_map {K L : SSet.{0}} (f : K ⟶ L) :
    Set.range (SSet.toTop.map f).hom =
      Set.range (SSet.toTop.map (SSet.Subcomplex.range f).ι).hom := by
…
```
theorem OAI.Thomason.Construction.RealizationPrism.compact_subset_stage line 585
Source documentation
A compact subset of an exhausted realization lies in one actual stage. The proof bounds its finitely many intrinsic carriers simultaneously.
```
theorem compact_subset_stage (K : SSet.{0}) (A : ℕ → K.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤)
    (C : Set (SSet.toTop.obj K)) (hC : IsCompact C) :
    ∃ n, C ⊆ Set.range (SSet.toTop.map (A n).ι).hom := by
…
```

theorem OAI.Thomason.Construction.RealizationPrism.compact_map_factors_stage line 615

Source documentation

Every compact continuous map factors continuously through a single stage, with exact equality after the actual inclusion.

theorem compact_map_factors_stage {P : Type} [TopologicalSpace P] [CompactSpace P]
    (K : SSet.{0}) (A : ℕ → K.Subcomplex) (hA : Monotone A) (hcover : iSup A = ⊤)
    (f : C(P, SSet.toTop.obj K)) :
    ∃ (n : ℕ) (g : C(P, SSet.toTop.obj (A n : SSet))),
      (SSet.toTop.map (A n).ι).hom.comp g = f := by
…

theorem OAI.Thomason.Construction.RealizationPrism.compact_map_factors_stage_after line 633

Source documentation

The stage can be chosen beyond any previously fixed stage.

theorem compact_map_factors_stage_after {P : Type} [TopologicalSpace P] [CompactSpace P]
    (K : SSet.{0}) (A : ℕ → K.Subcomplex) (hA : Monotone A) (hcover : iSup A = ⊤)
    (m : ℕ) (f : C(P, SSet.toTop.obj K)) :
    ∃ (n : ℕ), m ≤ n ∧ ∃ g : C(P, SSet.toTop.obj (A n : SSet)),
      (SSet.toTop.map (A n).ι).hom.comp g = f := by
…

theorem OAI.Thomason.Construction.RealizationPrism.compact_pair_factors_stage line 651

Source documentation

Two compact maps with unrelated domains have a common stage. This also synchronizes point representatives of different path components.

theorem compact_pair_factors_stage {P Q : Type}
    [TopologicalSpace P] [CompactSpace P] [TopologicalSpace Q] [CompactSpace Q]
    (K : SSet.{0}) (A : ℕ → K.Subcomplex) (hA : Monotone A) (hcover : iSup A = ⊤)
    (f : C(P, SSet.toTop.obj K)) (g : C(Q, SSet.toTop.obj K)) :
    ∃ (n : ℕ) (f' : C(P, SSet.toTop.obj (A n : SSet)))
      (g' : C(Q, SSet.toTop.obj (A n : SSet))),
      (SSet.toTop.map (A n).ι).hom.comp f' = f ∧
      (SSet.toTop.map (A n).ι).hom.comp g' = g := by
…

theorem OAI.Thomason.Construction.RealizationPrism.based_cube_factors_stage line 697

Source documentation

A based cube whose basepoint is already in one stage lifts to a later stage with that same basepoint and its entire boundary fixed.

theorem based_cube_factors_stage (K : SSet.{0}) (A : ℕ → K.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤) (m : ℕ)
    (x : SSet.toTop.obj (A m : SSet)) (d : ℕ)
    (p : GenLoop (Fin d) (SSet.toTop.obj K) ((SSet.toTop.map (A m).ι).hom x)) :
    ∃ (n : ℕ) (hn : m ≤ n),
      ∃ q : GenLoop (Fin d) (SSet.toTop.obj (A n : SSet))
        ((SSet.toTop.map (SSet.Subcomplex.homOfLE (hA hn))).hom x),
        ∀ t, (SSet.toTop.map (A n).ι).hom (q t) = p t := by
…

theorem OAI.Thomason.Construction.RealizationPrism.based_homotopy_factors_stage line 719

Source documentation

A homotopy between two cubes in one stage is already a homotopy in a later stage, with the original endpoint cubes and whole boundary retained.

theorem based_homotopy_factors_stage (K : SSet.{0}) (A : ℕ → K.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤) (m : ℕ)
    (x : SSet.toTop.obj (A m : SSet)) (d : ℕ)
    (p q : GenLoop (Fin d) (SSet.toTop.obj (A m : SSet)) x)
    (H : (HomotopyMaps.loopMap (SSet.toTop.map (A m).ι).hom p).val.HomotopyRel
      (HomotopyMaps.loopMap (SSet.toTop.map (A m).ι).hom q).val (Cube.boundary (Fin d))) :
    ∃ (n : ℕ) (hn : m ≤ n),
      Nonempty ((HomotopyMaps.loopMap
        (SSet.toTop.map (SSet.Subcomplex.homOfLE (hA hn))).hom p).val.HomotopyRel
        (HomotopyMaps.loopMap
          (SSet.toTop.map (SSet.Subcomplex.homOfLE (hA hn))).hom q).val
        (Cube.boundary (Fin d))) := by
…

Mentions: OAI.Thomason.Construction.HomotopyMaps.loopMap

theorem OAI.Thomason.Construction.RealizationPrism.homotopyGroup_eventual_eq line 753

Source documentation

Equality of homotopy classes in the exhausted realization is witnessed in one later stage, retaining the original chosen basepoint.

theorem homotopyGroup_eventual_eq (K : SSet.{0}) (A : ℕ → K.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤) (m : ℕ)
    (x : SSet.toTop.obj (A m : SSet)) (d : ℕ)
    (a b : HomotopyGroup.Pi d (SSet.toTop.obj (A m : SSet)) x)
    (hab : HomotopyMaps.groupMap (SSet.toTop.map (A m).ι).hom d x a =
      HomotopyMaps.groupMap (SSet.toTop.map (A m).ι).hom d x b) :
    ∃ (n : ℕ) (hn : m ≤ n),
      HomotopyMaps.groupMap (SSet.toTop.map (SSet.Subcomplex.homOfLE (hA hn))).hom d x a =
      HomotopyMaps.groupMap (SSet.toTop.map (SSet.Subcomplex.homOfLE (hA hn))).hom d x b := by
…

Mentions: OAI.Thomason.Construction.HomotopyMaps.groupMap

theorem OAI.Thomason.Construction.RealizationPrism.components_eventual_eq line 773

Source documentation

Equality of components also occurs at a finite stage.

theorem components_eventual_eq (K : SSet.{0}) (A : ℕ → K.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤) (m : ℕ)
    (a b : ZerothHomotopy (SSet.toTop.obj (A m : SSet)))
    (hab : HomotopyMaps.componentsMap (SSet.toTop.map (A m).ι).hom a =
      HomotopyMaps.componentsMap (SSet.toTop.map (A m).ι).hom b) :
    ∃ (n : ℕ) (hn : m ≤ n),
      HomotopyMaps.componentsMap (SSet.toTop.map (SSet.Subcomplex.homOfLE (hA hn))).hom a =
      HomotopyMaps.componentsMap (SSet.toTop.map (SSet.Subcomplex.homOfLE (hA hn))).hom b := by
…

Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap

theorem OAI.Thomason.Construction.RealizationPrism.based_pair_factors_stage line 807

Source documentation

A pair of based cubes can be placed in the same stage, beyond the stage of their specified basepoint. Both cubes retain their entire boundary.

theorem based_pair_factors_stage (K : SSet.{0}) (A : ℕ → K.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤) (m : ℕ)
    (x : SSet.toTop.obj (A m : SSet)) (d : ℕ)
    (p q : GenLoop (Fin d) (SSet.toTop.obj K) ((SSet.toTop.map (A m).ι).hom x)) :
    ∃ (n : ℕ) (hn : m ≤ n),
      ∃ p' q' : GenLoop (Fin d) (SSet.toTop.obj (A n : SSet))
        ((SSet.toTop.map (SSet.Subcomplex.homOfLE (hA hn))).hom x),
        (∀ t, (SSet.toTop.map (A n).ι).hom (p' t) = p t) ∧
        (∀ t, (SSet.toTop.map (A n).ι).hom (q' t) = q t) := by
…

theorem OAI.Thomason.Construction.RealizationPrism.exhaustion_initial_weak line 868
Source documentation
If the inclusion of the initial stage into every stage is weak, then its inclusion into the exhausted realization is weak. Compact cubes and relative homotopies provide the required finite-stage witnesses.
```
theorem exhaustion_initial_weak (K : SSet.{0}) (A : ℕ → K.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤)
    (hW : ∀ n, realizationWeakEquivalences
      (SSet.Subcomplex.homOfLE (hA (Nat.zero_le n)))) :
    realizationWeakEquivalences (A 0).ι := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.RealizationPrism.exhaustion_weak_of_successor line 946
Source documentation
Successive weak inclusions in a simplicial exhaustion induce a weak inclusion of its initial stage into the whole realization.
```
theorem exhaustion_weak_of_successor (K : SSet.{0}) (A : ℕ → K.Subcomplex)
    (hA : Monotone A) (hcover : iSup A = ⊤)
    (hW : ∀ n, realizationWeakEquivalences
      (SSet.Subcomplex.homOfLE (hA (Nat.le_succ n)))) :
    realizationWeakEquivalences (A 0).ι := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences