instPartialOrderSubtypeProdAndEqHMulFstSndOfNatHAdd

English

There is a natural partial order on E, defined by the property that a ≤ b iff a.1.1 ≤ b.1.1 in the underlying coordinates, compatible with the product structure.

Русский

Существует естественный частичный порядок на E, задаваемый по свойству a ≤ b тогда, когда координаты базового элемента удовлетворяют соответствующему порядку.

LaTeX

$$$\le$ на $E = \{(a,b) \in R \times R \mid ab=0, a+b=1\}$ определяется совместно с координатами так, чтобы оно соответствовало порядку на произведении.$$

Lean4

instance : PartialOrder { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
    where
  le a b := a.1.1 * b.1.1 = a.1.1
  le_refl a := (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1
  le_trans a b c hab hbc := show _ = _ by rw [← hab, mul_assoc, hbc]
  le_antisymm a b hab hba := mul_eq_zero_add_eq_one_ext_left <| by rw [← hab, mul_comm, hba]

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