fintypeNodupList — Mathlib

English

There is a finite type consisting of all lists with nodup property, i.e., the type { l : List α // l.Nodup } is finite.

Русский

Существует конечный тип, содержащий все списки с свойством Nodup, то есть { l : List α // l.Nodup } конечен.

LaTeX

$$$\\text{Fintype }\\{ l : List\\ α \\ // l.Nodup \\}$$$

Lean4

instance fintypeNodupList [Fintype α] : Fintype { l : List α // l.Nodup } :=
  by
  refine Fintype.ofFinset ?_ ?_
  · let univSubsets := ((Finset.univ : Finset α).powerset.1 : (Multiset (Finset α)))
    let allPerms := Multiset.bind univSubsets (fun s => (Multiset.lists s.1))
    refine ⟨allPerms, Multiset.nodup_bind.mpr ?_⟩
    simp only [Multiset.lists_nodup_finset, implies_true, true_and]
    unfold Multiset.Pairwise
    use ((Finset.univ : Finset α).powerset.toList : (List (Finset α)))
    constructor
    · simp only [Finset.coe_toList]
      rfl
    · convert Finset.nodup_toList (Finset.univ.powerset : Finset (Finset α))
      ext l
      unfold Nodup
      refine Pairwise.iff ?_
      intro m n
      simp only [_root_.Disjoint]
      rw [← m.coe_toList, ← n.coe_toList, Multiset.lists_coe, Multiset.lists_coe]
      have := Multiset.coe_disjoint m.toList.permutations n.toList.permutations
      rw [_root_.Disjoint] at this
      rw [this]
      simp only [ne_eq]
      rw [List.disjoint_iff_ne]
      constructor
      · intro h
        by_contra hc
        rw [hc] at h
        contrapose! h
        use n.toList
        simp
      · intro h
        simp only [mem_permutations]
        intro a ha b hb
        by_contra hab
        absurd h
        rw [hab] at ha
        exact Finset.perm_toList.mp <| Perm.trans ha.symm hb
  · intro l
    simp only [Finset.mem_mk, Multiset.mem_bind, Finset.mem_val, Finset.mem_powerset, Finset.subset_univ,
      Multiset.mem_lists_iff, Multiset.quot_mk_to_coe, true_and]
    constructor
    · intro h
      rcases h with ⟨f, hf⟩
      convert f.nodup
      rw [hf]
      rfl
    · intro h
      exact CanLift.prf _ h

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