def
definition
refl
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Core.Octave on GitHub at line 101.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
98namespace OctaveEquiv
99
100/-- Reflexivity. -/
101def refl (O : Octave) : OctaveEquiv O O where
102 toFun := OctaveMorphism.id O
103 invFun := OctaveMorphism.id O
104 strain_eq := fun _ => rfl
105 strain_eq_inv := fun _ => rfl
106
107/-- Symmetry. -/
108def symm {O₁ O₂ : Octave} (e : OctaveEquiv O₁ O₂) : OctaveEquiv O₂ O₁ where
109 toFun := e.invFun
110 invFun := e.toFun
111 strain_eq := e.strain_eq_inv
112 strain_eq_inv := e.strain_eq
113
114end OctaveEquiv
115
116/-- The "octave index" in Z (integer rung number).
117 This is just a type alias; the physical interpretation is in Hypotheses. -/
118abbrev OctaveRung := ℤ
119
120/-- A family of octaves indexed by rung. -/
121structure OctaveFamily where
122 /-- The octave at each rung. -/
123 octaveAt : OctaveRung → Octave
124
125end RRF.Core
126end IndisputableMonolith