instLinearOrderedCommMonoidWithZeroElemReal

English

The type of unit interval elements, with the inherited multiplication and order, carries a LinearOrderedCommMonoidWithZero structure.

Русский

Тип элементов единичного интервала, с унаследованным умножением и порядком, образует линейно упорядоченный коммутативный моноид с нулём.

LaTeX

$$UnitInterval.Elem forms a LinearOrderedCommMonoidWithZero.$$

Lean4

instance : LinearOrderedCommMonoidWithZero I
    where
  zero_mul i := zero_mul i
  mul_zero i := mul_zero i
  zero_le_one := nonneg'
  mul_le_mul_left i j h_ij
    k := by
    simp only [← Subtype.coe_le_coe, coe_mul]
    apply mul_le_mul le_rfl ?_ (nonneg i) (nonneg k)
    simp [h_ij]

Похожие утверждения