ForMatUS: Monotonía de la multiplicación por no negativo (en Lean)
En el vídeo se comentan 6 demostraciones en Lean de la siguiente propiedad:
Sean a, b y c números reales. Si 0 ≤ c y a ≤ b, entonces ac ≤ bc.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo