Stream: maths

Topic: finset.inter

Kevin Buzzard (Feb 16 2020 at 16:12):

import data.finset

/-
From data.finset:

/-- s ∩ t is the set such that a ∈ s ∩ t iff a ∈ s and a ∈ t. -/
instance : has_inter (finset α) := ⟨λ s₁ s₂, ⟨_, nodup_ndinter s₂.1 s₁.2⟩⟩

-/

instance (X : Type*) : has_inter (finset X) := by apply_instance -- fails


Why can't I intersect finite sets?

Chris Hughes (Feb 16 2020 at 16:12):

decidable equality

rofl

thanks again

Kevin Buzzard (Feb 16 2020 at 16:14):

PS I'd just got there myself -- the annoying part is guessing the name of the instance because it's never explicitly named in mathlib. Could the name of the instance be put in the comments or is that crazy?

Kevin Buzzard (Feb 16 2020 at 16:14):

It wasn't hard to guess this time, but it's the only way I know of debugging these things

Floris van Doorn (Feb 17 2020 at 20:53):

You can run #print instances has_inter to find the name.

Last updated: May 14 2021 at 19:21 UTC