Smul interference
ConNF.BasePerm.smul_interference
Plain-language statement
Base permutations commute with the interference of near-litters.
Exact Lean statement
@[simp]
theorem smul_interference (π : BasePerm) (N₁ N₂ : NearLitter) :
π • interference N₁ N₂ = interference (π • N₁) (π • N₂)Formal artifact
Lean source
@[simp]theorem smul_interference (π : BasePerm) (N₁ N₂ : NearLitter) : π • interference N₁ N₂ = interference (π • N₁) (π • N₂) := by by_cases h : N₁ᴸ = N₂ᴸ · rw [interference_eq_of_litter_eq h, interference_eq_of_litter_eq, Set.smul_set_symmDiff, smul_nearLitter_atoms, smul_nearLitter_atoms] rwa [smul_nearLitter_litter, smul_nearLitter_litter, smul_left_cancel_iff] · rw [interference_eq_of_litter_ne h, interference_eq_of_litter_ne, Set.smul_set_inter, smul_nearLitter_atoms, smul_nearLitter_atoms] rwa [smul_nearLitter_litter, smul_nearLitter_litter, ne_eq, smul_left_cancel_iff]- Project
- Con(NF)
- License
- Apache-2.0
- Commit
- 55b939a3acf9
- Source
- ConNF/Base/BasePerm.lean:202-211
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.
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.
Str Action flex Approx coherent
ConNF.StrAction.flexApprox_coherent
Plain-language statement
TODO: Put this in the blueprint.
Source project: Con(NF)
Person-level attribution pending.