Freedom of action for structural actions #
In this file, we state and prove the freedom of action theorem for structural actions.
Main declarations #
ConNF.StrAction.freedomOfAction: Freedom of action for structural actions.
def
ConNF.StrAction.FreedomOfAction
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
(β : ConNF.TypeIndex)
[ConNF.LeLevel β]
:
Equations
- ConNF.StrAction.FreedomOfAction β = ∀ (ξ : ConNF.StrAction β), ξ.Coherent → ∃ (ρ : ConNF.AllPerm β), ξ.Approximates ρ
Instances For
theorem
ConNF.StrAction.approximates_of_flexApprox_exactlyApproximates
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{ξ : ConNF.StrAction β}
(hξ : ξ.Coherent)
{ρ : ConNF.AllPerm β}
(hρ : ξ.flexApprox.ExactlyApproximates ρ)
:
ξ.Approximates ρ
theorem
ConNF.StrAction.freedomOfAction
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
: