isTotal_left — Mathlib

English

If α is totally ordered by r, then the lex order on α×β is total on the left component.

Русский

Если α полностью упорядочено по r, то лексикографический порядок на α×β тотален по левой координате.

LaTeX

$$[IsTotal α r] : IsTotal (α × β) (Prod.Lex r s)$$

Lean4

instance isTotal_left {r : α → α → Prop} {s : β → β → Prop} [IsTotal α r] : IsTotal (α × β) (Prod.Lex r s) :=
  ⟨fun ⟨a₁, _⟩ ⟨a₂, _⟩ ↦ (IsTotal.total a₁ a₂).imp (Lex.left _ _) (Lex.left _ _)⟩

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