leAdd — Mathlib

English

An initial segment embedding from r into the Lexicographic sum Sum.Lex r s exists; it sends a to the left injection Sum.inl a.

Русский

Существует вложение начального сегмента из r в Sum.Lex r s, которое отправляет a в Sum.inl a.

LaTeX

$$$leAdd(r,s) : r \\preccurlyeq_i Sum.Lex\\, r\\, s.$$$

Lean4

/-- Initial segment embedding of an order `r` into the disjoint union of `r` and `s`. -/
def leAdd (r : α → α → Prop) (s : β → β → Prop) : r ≼i Sum.Lex r s :=
  ⟨⟨⟨Sum.inl, fun _ _ => Sum.inl.inj⟩, Sum.lex_inl_inl⟩, fun a b => by
    cases b <;> [exact fun _ => ⟨_, rfl⟩; exact False.elim ∘ Sum.lex_inr_inl]⟩

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