allRoots_subset_range_root — Mathlib

English

The finite subset of M consisting of allRoots(P) lies inside the range of the root map P.root.

Русский

Конечный подпорядок в M, состоящий из allRoots(P), вложен в образ отображения корня P.root.

LaTeX

$$$\{\text{allRoots}(P)\} \subseteq \operatorname{range}(P.root)$$$

Lean4

theorem allRoots_subset_range_root [DecidableEq M] : ↑(allRoots P).toFinset ⊆ range P.root :=
  by
  intro x hx
  simp only [toFinset_cons, toFinset_nil, insert_empty_eq, Finset.coe_insert, Finset.coe_singleton, mem_insert_iff,
    mem_singleton_iff] at hx
  rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp

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