instFintypeSubtypeListProdBoolRed

English

For a fixed L1, the set { L2 | Red L1 L2 } carries a finite type structure.

Русский

Для фиксированного L1 множество { L2 | Red L1 L2 } является конечным типом.

LaTeX

$$$\text{(L}_1 : List(\alpha \times Bool)) \Rightarrow\; \text{Fintype} \{ L_2 \;\vert\; Red L_1 L_2 \}$$$

Lean4

instance (L₁ : List (α × Bool)) : Fintype { L₂ // Red L₁ L₂ } :=
  Fintype.subtype (List.toFinset <| Red.enum L₁) fun _L₂ =>
    ⟨fun H => Red.enum.sound <| List.mem_toFinset.1 H, fun H => List.mem_toFinset.2 <| Red.enum.complete H⟩

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