Str Action flex Approx coherent
ConNF.StrAction.flexApprox_coherent
Plain-language statement
TODO: Put this in the blueprint.
Exact Lean statement
theorem StrAction.flexApprox_coherent [Level] {β : TypeIndex} [LeLevel β] [CoherentData]
(ξ : StrAction β) (hξ : ∀ A, (ξ A).MapFlexible A) :
StrApprox.Coherent ξ.flexApproxFormal artifact
Lean source
theorem StrAction.flexApprox_coherent [Level] {β : TypeIndex} [LeLevel β] [CoherentData] (ξ : StrAction β) (hξ : ∀ A, (ξ A).MapFlexible A) : StrApprox.Coherent ξ.flexApprox := by intro A L₁ L₂ hL constructor · intro P t hA ht cases ((ξ A).flexApprox_flexApprox (hξ A)).flexible_of_mem_dom ⟨L₂, hL⟩ ⟨P, t, hA, ht⟩ · intro _ apply ((ξ A).flexApprox_flexApprox (hξ A)).flexible_of_mem_dom rw [← (BaseApprox.litters_permutative _).codom_eq_dom] exact ⟨L₁, hL⟩- Project
- Con(NF)
- License
- Apache-2.0
- Commit
- 55b939a3acf9
- Source
- ConNF/FOA/StrAction.lean:80-90
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Smul near Litter of smul litter
ConNF.BaseAction.smul_nearLitter_of_smul_litter
Project documentation
The main lemma about how approximations interact with actions.
Source project: Con(NF)
Person-level attribution pending.
Smul interference
ConNF.BasePerm.smul_interference
Plain-language statement
Base permutations commute with the interference of near-litters.
Source project: Con(NF)
Person-level attribution pending.
Card t Set le
ConNF.card_tSet_le
Plain-language statement
Note that we cannot prove the reverse implication because all of our hypotheses at this stage are about permutations, not objects.
Source project: Con(NF)
Person-level attribution pending.