Theorems · Definition · dynamical systems
SymbolicDynamics.FullShift.Pattern.support
{A : Type u_1} → {G : Type u_2} → [inst : Inhabited A] → SymbolicDynamics.FullShift.Pattern A G → Finset GFinite support of the pattern.
- Defined in
- Mathlib.Dynamics.SymbolicDynamics.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- Inhabited
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- SymbolicDynamics.FullShift.Patternstatement and proof · cited by 21
Cited by17
Results whose statement or proof uses this declaration.
- SymbolicDynamics.FullShift.Pattern.mulOccursInAtproof · cited by 6
- SymbolicDynamics.FullShift.Pattern.occursInAtproof · cited by 6
- SymbolicDynamics.FullShift.Pattern.mulShiftproof · cited by 4
- SymbolicDynamics.FullShift.Pattern.shiftproof · cited by 4
- SymbolicDynamics.FullShift.mulOccursInAt_eq_cylinderstatement and proof · cited by 2
- SymbolicDynamics.FullShift.occursInAt_eq_cylinderstatement and proof · cited by 2
- SymbolicDynamics.FullShift.finite_setOfPred_pattern_support_eqstatement and proof · cited by 1
- SymbolicDynamics.FullShift.isOpen_mulOccursInAtproof · cited by 1
- SymbolicDynamics.FullShift.isOpen_occursInAtproof · cited by 1
- SymbolicDynamics.FullShift.Pattern.mulShift_apply_mul_left_of_memstatement and proof · cited by 1
- SymbolicDynamics.FullShift.Pattern.occursInAt_shiftproof · cited by 1
- SymbolicDynamics.FullShift.Pattern.shift_apply_add_left_of_memstatement and proof · cited by 1