le_induce_union — Mathlib

English

The join (supremum) of inductions on s and s' is below the induction on s ∪ s'.

Русский

Сумма индукций на s и s' не превосходит индукцию на s ∪ s'.

LaTeX

$$$ G'.induce s \\sqcup G'.induce s' \\le G'.induce (s \\cup s') $$$

Lean4

theorem le_induce_union : G'.induce s ⊔ G'.induce s' ≤ G'.induce (s ∪ s') :=
  by
  constructor
  · simp only [verts_sup, induce_verts, Set.Subset.rfl]
  · simp only [sup_adj, induce_adj, Set.mem_union]
    rintro v w (h | h) <;> simp [h]

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