mem_factorSet_some — Mathlib

English

Let l be a multiset of irreducibles represented as Subtype elements. For p irreducible, p ∈ (l : FactorSet α) if and only if the pair ⟨p, hp⟩ belongs to l.

Русский

Пусть l — мультисет неприводимых, представленная как элементы-подтипы. Тогда p ∈ (l : FactorSet α) тогда и только если пара ⟨p, hp⟩ принадлежит l.

LaTeX

$$$p \\in (l : \\mathrm{FactorSet}(\\alpha)) \\iff \\mathrm{Subtype.mk}\\\\ p\\\\ hp \\in l$$$

Lean4

theorem mem_factorSet_some {p : Associates α} {hp : Irreducible p}
    {l : Multiset { a : Associates α // Irreducible a }} : p ∈ (l : FactorSet α) ↔ Subtype.mk p hp ∈ l := by
  dsimp only [Membership.mem]; dsimp only [FactorSetMem]; split_ifs; rfl

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