Induced action: Atoms #
In this file, we describe the induced action of an approximation on atoms.
Main declarations #
ConNF.StructApprox.atomCompletion: The induced action of a structural approximation on an atom.
theorem
ConNF.StructApprox.equiv_apply_mem
[ConNF.Params]
{S : ConNF.Sublitter}
{T : ConNF.Sublitter}
{a : ↥S}
{L : ConNF.Litter}
(h : ↑((S.equiv T) a) ∈ ConNF.litterSet L)
:
T.litter = L
theorem
ConNF.StructApprox.equiv_apply_eq
[ConNF.Params]
{S : ConNF.Sublitter}
{T : ConNF.Sublitter}
{U : ConNF.Sublitter}
{V : ConNF.Sublitter}
{a : ↥S}
{b : ↥U}
(h : ↑((S.equiv T) a) = ↑((U.equiv V) b))
:
T.litter = V.litter
noncomputable def
ConNF.StructApprox.atomCompletion
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.FOAAssumptions]
{β : ConNF.Λ}
(π : ConNF.StructApprox ↑β)
(A : ConNF.ExtendedIndex ↑β)
(a : ConNF.Atom)
(H : ConNF.HypAction { path := A, value := Sum.inl a })
:
ConNF.Atom
Computes the action of a structural approximation π on an atom a.
Equations
- One or more equations did not get rendered due to their size.