Zulip Chat Archive

Stream: new members

Topic: How to do Finset (Finset Type) instead of Set (Finset Type)


Icaro Costa (Aug 04 2025 at 16:02):

How do I make these definitions have type Finset (Finset Type) instead of Set (Finset Type)?

import Mathlib
open Nat
open Finset

variable {N k: ℕ}(hk: k ≤ N)(hk2: k ≥ 2)
variable {V : Finset ℕ} (hV : V ⊆ Finset.range N)

def U (a b : V) (k : ℕ) := {X : Finset V | ({a,b} ∩ X ≠ ∅) ∧ (X.card = k)}

Aaron Liu (Aug 04 2025 at 16:04):

def U (a b : V) (k : ℕ) : Finset (Finset V) := {X : Finset V | ({a,b} ∩ X ≠ ∅) ∧ (X.card = k)}

Icaro Costa (Aug 04 2025 at 16:05):

Oh right, sorry for the stupid question

Kenny Lau (Aug 04 2025 at 16:23):

this is why you should always indicate the type in a def


Last updated: Feb 28 2026 at 14:05 UTC