Code

feat: constructible sets#20054

Code

Open

YaelDillies wants to merge 9 commits intomasterleanprover-community/mathlib4:masterfrom constructible_setleanprover-community/mathlib4:constructible_setCopy head branch name to clipboard

+445-1

Commits

Commits on Jan 7, 2025

• feat: constructible sets

  Show description for 79547e1
  YaelDillies

  committed
  79547e1

  Copy full SHA for 79547e1

• more explanation

  YaelDillies

  committed
  6df7a24

  Copy full SHA for 6df7a24

• suggestions

  YaelDillies

  committed
  f090630

  Copy full SHA for f090630

• use Set (Set X)

  YaelDillies

  committed
  df3bcca

  Copy full SHA for df3bcca

• typo

  Show description for 5a5a028
  

  YaelDillies

  and

  alreadydone

  committed
  5a5a028

  Copy full SHA for 5a5a028

• Junyan's comments

  YaelDillies

  committed
  e69305c

  Copy full SHA for e69305c

• correct definition of locally constructible

  YaelDillies

  committed
  9524eae

  Copy full SHA for 9524eae

• more lemmas

  YaelDillies

  committed
  0b689e8

  Copy full SHA for 0b689e8

• fix

  YaelDillies

  committed
  c2b4440

  Copy full SHA for c2b4440