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.
Equations
- ConNF.StrAction.FreedomOfAction β = ∀ (ξ : ConNF.StrAction β), ξ.Coherent → ∃ (ρ : ConNF.AllPerm β), ξ.Approximates ρ
Instances For
theorem
ConNF.StrAction.approximates_of_flexApprox_exactlyApproximates
[Params]
[Level]
[CoherentData]
{β : TypeIndex}
[LeLevel β]
{ξ : StrAction β}
(hξ : ξ.Coherent)
{ρ : AllPerm β}
(hρ : ξ.flexApprox.ExactlyApproximates ρ)
:
ξ.Approximates ρ
theorem
ConNF.StrAction.freedomOfAction
[Params]
[Level]
[CoherentData]
{β : TypeIndex}
[LeLevel β]
: