union_eq_right — Mathlib

English

Let α be a type and xs, ys be lists over α. If xs is contained in ys (xs ⊆ ys), then xs ∪ ys = ys.

Русский

Пусть α — тип, xs и ys — списки по α. Если xs ⊆ ys, то xs ∪ ys = ys.

LaTeX

$$$\\\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] {xs, ys : \\\\mathrm List \\\\alpha},\n xs \\\\subseteq ys \\\rightarrow xs \\\\cup ys = ys$$$

Lean4

theorem union_eq_right {xs ys : List α} (h : xs ⊆ ys) : xs ∪ ys = ys := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self, ih <| subset_of_cons_subset h]

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