instFintypeElemProdNatSetOfLtSndCountFst

English

There exists a finite type structure on the set {p : α × ℕ | p.2 < m.count p.1}.

Русский

Существует конечный тип для множества {p ∈ α × ℕ | p.2 < m.count p.1}.

LaTeX

$$$\text{Fintype}\{ p \in \alpha \times \mathbb{N} \mid p_2 < \mathrm{count}(p_1, m) \}$$$

Lean4

instance : Fintype {p : α × ℕ | p.2 < m.count p.1} :=
  Fintype.ofFinset (m.toFinset.biUnion fun x ↦ (Finset.range (m.count x)).map ⟨_, Prod.mk_right_injective x⟩)
    (by
      rintro ⟨x, i⟩
      simp only [Finset.mem_biUnion, Multiset.mem_toFinset, Finset.mem_map, Finset.mem_range,
        Function.Embedding.coeFn_mk, Prod.mk_inj, Set.mem_setOf_eq]
      simp only [← and_assoc, exists_eq_right, and_iff_right_iff_imp]
      exact fun h ↦ Multiset.count_pos.mp (by cutsat))

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