Constant coherent protected chains #
noncomputable def
ScottishBook155.constantProtectedChain
{ι : Type u}
[LinearOrder ι]
{r L : ℝ}
(S : ProtectedStage r)
:
ProtectedChain r L
A constant family of one protected stage is a coherent chain.
Equations
- One or more equations did not get rendered due to their size.