Union of finsets

Stream: maths

[GENNARO PORPORA]

Hi all, i cant make the union of two finsets hset1 and hset2, why ? :sob: Here the code

lemma inter_politopes (plt1 plt2: Polytope (𝕜:=𝕜)):
      isPolytope (𝕜:=𝕜) (V:=V) (plt1.carrier ∩ plt2.carrier) := by
  have isp1: isPolytope (𝕜:=𝕜) plt1.carrier := by
      use plt1.vertices
      exact plt1.is_convex
  have isp2: isPolytope (𝕜:=𝕜) plt2.carrier := by
      use plt2.vertices
      exact plt2.is_convex

  rcases ((poly_iff_inter plt1.carrier).mp isp1) with ⟨hset1, hp1⟩
  rcases ((poly_iff_inter plt2.carrier).mp isp2) with ⟨hset2, hp2⟩
  have is_inter : ∃(Hset3: Finset (Set V)), ∀hsp ∈ Hset3,
                  isHalfSpace (𝕜:=𝕜) hsp ∧
                  plt1.carrier ∩ plt2.carrier = ⋂ hsp ∈ Hset3, hsp := by

      -- lean says failed to synthetize (Finset (Set V)), WHY ?
      let hset3 := hset1 ∪ hset2


  apply (poly_iff_inter (plt1.carrier ∩ plt2.carrier)).mpr is_inter
```

```

[Matt Diamond]

could you post a #mwe?

also what are the types of hset1 and hset2?

[Matt Diamond]

one gotcha with Finset unions is that they require decidable equality (see docs#Finset.instUnion)

[Matt Diamond]

this isn't a big deal though... you can just write classical let hset3 := hset1 ∪ hset2

[GENNARO PORPORA]

:astonished: with classical it wooorks ! Thank you so much !! :yellow_heart:

[Notification Bot]

5 messages were moved here from #maths > Piecewise linear maps by Ruben Van de Velde.