structure
definition
def or abbrev
L4DerivableCert
show as:
view Lean formalization →
formal statement (Lean)
185structure L4DerivableCert (𝒞 : Type*) where
186 l4_from_recognizer :
187 ∀ m : MultiplicativeRecognizer 𝒞,
188 ∃ P : ℝ → ℝ → ℝ,
189 ∀ x y : ℝ, 0 < x → 0 < y →
190 m.cost (x * y) + m.cost (x / y) = P (m.cost x) (m.cost y)
191 l4_polynomial_form :
192 ∀ m : MultiplicativeRecognizer 𝒞,
193 MultiplicativeL4Polynomial m
194 identity_at_one :
195 ∀ m : MultiplicativeRecognizer 𝒞, m.cost 1 = 0
196 reciprocal_symmetry :
197 ∀ m : MultiplicativeRecognizer 𝒞,
198 ∀ x : ℝ, 0 < x → m.cost x = m.cost (x⁻¹)
199