structure
definition
def or abbrev
ConditionalCompletionRoute
show as:
view Lean formalization →
formal statement (Lean)
107structure ConditionalCompletionRoute (α : Type) where
108 FRC : α → Prop
109 InjectionDamping : α → Prop
110 DirectionConstancy : α → Prop
111 RigidRotationVeto : α → Prop
112 Regularity : α → Prop
113 frc_to_injectionDamping : ∀ a, FRC a → InjectionDamping a
114 injectionDamping_to_directionConstancy : ∀ a, InjectionDamping a → DirectionConstancy a
115 directionConstancy_to_rigidRotationVeto : ∀ a, DirectionConstancy a → RigidRotationVeto a
116 rigidRotationVeto_to_regularity : ∀ a, RigidRotationVeto a → Regularity a
117
118/-- Once FRC is known on the lattice, any conditional-completion route closes. -/