English
type (Prod.Lex s r) equals type r times type s.
Русский
Тип (Prod.Lex s r) равен произведению типов r и s.
LaTeX
$$type(Prod.Lex(s,r)) = type(r) \cdot type(s)$$
Lean4
/-- The multiplication of ordinals `o₁` and `o₂` is the (well-founded) lexicographic order on
`o₂ × o₁`. -/
instance monoid : Monoid Ordinal.{u}
where
mul a
b :=
Quotient.liftOn₂ a b
(fun ⟨α, r, _⟩ ⟨β, s, _⟩ => ⟦⟨β × α, Prod.Lex s r, inferInstance⟩⟧ : WellOrder → WellOrder → Ordinal)
fun ⟨_, _, _⟩ _ _ _ ⟨f⟩ ⟨g⟩ => Quot.sound ⟨RelIso.prodLexCongr g f⟩
one := 1
mul_assoc a b
c :=
Quotient.inductionOn₃ a b c fun ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨γ, t, _⟩ =>
Eq.symm <|
Quotient.sound
⟨⟨prodAssoc _ _ _,
@fun a b => by
rcases a with ⟨⟨a₁, a₂⟩, a₃⟩
rcases b with ⟨⟨b₁, b₂⟩, b₃⟩
simp [Prod.lex_def, and_or_left, or_assoc, and_assoc]⟩⟩
mul_one
a :=
inductionOn a fun α r _ =>
Quotient.sound
⟨⟨punitProd _,
@fun a b => by
rcases a with ⟨⟨⟨⟩⟩, a⟩; rcases b with ⟨⟨⟨⟩⟩, b⟩
simp only [Prod.lex_def, EmptyRelation, false_or]
simp only [true_and]
rfl⟩⟩
one_mul
a :=
inductionOn a fun α r _ =>
Quotient.sound
⟨⟨prodPUnit _,
@fun a b => by
rcases a with ⟨a, ⟨⟨⟩⟩⟩; rcases b with ⟨b, ⟨⟨⟩⟩⟩
simp only [Prod.lex_def, EmptyRelation, and_false, or_false]
rfl⟩⟩
