feat(Data/Finset/Card): of cardinality between by madvorak · Pull Request #20433 · leanprover-community/mathlib4

madvorak · 2025-01-03T12:40:15Z

github-actions · 2025-01-03T12:41:07Z

PR summary 61b2a51af5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ of_cardinality_between_of_disjoint

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

alreadydone · 2025-01-03T14:35:10Z

+lemma of_cardinality_between_of_disjoint (hs : #s < n) (hn : n ≤ #s + #t) (hst : Disjoint s t) :
+    ∃ (x : Finset α) (hxs : Disjoint x s), #(x.disjUnion s hxs) = n ∧ Nonempty x := by


I think we should be satisfied with this statement:

Suggested change

lemma of_cardinality_between_of_disjoint (hs : #s < n) (hn : n ≤ #s + #t) (hst : Disjoint s t) :

∃ (x : Finset α) (hxs : Disjoint x s), #(x.disjUnion s hxs) = n ∧ Nonempty x := by

lemma of_cardinality_between_of_disjoint (hs : #s ≤ n) (hn : n ≤ #s + #t) (hst : Disjoint s t) :

∃ (x : Finset α) (hxs : Disjoint x s), #(x.disjUnion s hxs) = n := by

because nonemptiness can be easily deduced from this:

import Mathlib open Finset in example {n} {α} (s x : Finset α) (hxs : Disjoint x s) (eq : #(x.disjUnion s hxs) = n) (lt : #s < n) : x ≠ ∅ := by rintro rfl; rw [← eq] at lt; simp at lt

(Note I've replaced Nonempty x with x ≠ ∅.)

For the purposes of #19607 I prefer the stronger version.

Do you want to have both lemmas?

Yes please; and please use the x ≠ ∅ statement: from the lemmas around Finset.nonempty_iff_ne_empty I think statements involving ∅ are considered the normal form.

Pinging @YaelDillies for a second opinion on whether that or Nonempty is preferred.

YaelDillies · 2025-01-05T13:44:47Z

I don't really see the point of this lemma. Why can't you directly use Finset.exists_subset_card_eq? Your new lemma isn't (yet) used in #19607, so I can't really offer you a more precise replacement for it.

madvorak · 2025-01-06T17:43:10Z

I don't really see the point of this lemma. Why can't you directly use Finset.exists_subset_card_eq? Your new lemma isn't (yet) used in #19607, so I can't really offer you a more precise replacement for it.

You are right I don't use the new lemma. The lemma I use at the moment is:

import Mathlib.Tactic

lemma finset_of_cardinality_between {α β : Type*} [Fintype α] [Fintype β] {n : ℕ}
    (hα : Fintype.card α < n) (hn : n ≤ Fintype.card α + Fintype.card β) :
    ∃ b : Finset β, Fintype.card (α ⊕ b) = n ∧ Nonempty b := by
  have beta' : n - Fintype.card α ≤ Fintype.card β
  · omega
  obtain ⟨s, hs⟩ : ∃ s : Finset β, s.card = n - Fintype.card α :=
    (Finset.exists_subset_card_eq beta').imp (by simp)
  use s
  rw [Fintype.card_sum, Fintype.card_coe, hs]
  constructor
  · omega
  · by_contra ifempty
    have : s.card = 0
    · rw [Finset.card_eq_zero]
      rw [nonempty_subtype, not_exists] at ifempty
      exact Finset.eq_empty_of_forall_not_mem ifempty
    omega

It will probably change after the refactor suggested by Kevin Buzzard.

madvorak · 2025-01-06T17:44:25Z

Can you @YaelDillies nevertheless clarify whether Nonempty x or x ≠ ∅ is preferred?

YaelDillies · 2025-01-06T19:31:26Z

I don't use the new lemma. The lemma I use at the moment is: [...]. It will probably change after the refactor suggested by Kevin Buzzard.

Ah okay, then I suggest we leave that PR unmerged for the time being, until what you actually need becomes clearer

Can you @YaelDillies nevertheless clarify whether Nonempty x or x ≠ ∅ is preferred?

x.Nonempty is preferred

madvorak · 2025-01-06T19:39:19Z

Yes. All four PRs are labelled as WIP now.

madvorak · 2025-01-13T13:51:02Z

In the end, I will need exactly this lemma:

lemma finset_of_cardinality_between {α β : Type*} [Fintype α] [Fintype β] {n : ℕ}
    (hα : Fintype.card α < n) (hn : n ≤ Fintype.card α + Fintype.card β) :
    ∃ b : Finset β, Fintype.card (α ⊕ b) = n ∧ Nonempty b := by
  have beta' : n - Fintype.card α ≤ Fintype.card β
  · omega
  obtain ⟨s, hs⟩ : ∃ s : Finset β, s.card = n - Fintype.card α :=
    (Finset.exists_subset_card_eq beta').imp (by simp)
  use s
  rw [Fintype.card_sum, Fintype.card_coe, hs]
  constructor
  · omega
  · by_contra ifempty
    have : s.card = 0
    · rw [Finset.card_eq_zero]
      rw [nonempty_subtype, not_exists] at ifempty
      exact Finset.eq_empty_of_forall_not_mem ifempty
    omega

Do you @YaelDillies want to weigh in on how it should be generalized for Mathlib? Finset version perhaps?

YaelDillies · 2025-01-22T15:23:53Z

This lemma is overly specific, I find, so I think you should inline it where needed.

Here's a golf, using new machinery that could belong in mathlib:

import Mathlib.Data.Fintype.Sum

namespace Equiv
variable {α β : Type*}

-- Analogue of `Equiv.optionIsSomeEquiv`
@[simps]
def sumIsLeft : {x : α ⊕ β // x.isLeft} ≃ α where
  toFun x := x.1.getLeft x.2
  invFun a := ⟨.inl a, Sum.isLeft_inl⟩
  left_inv | ⟨.inl _a, _⟩ => rfl
  right_inv _a := rfl

@[simps]
def sumIsRight : {x : α ⊕ β // x.isRight} ≃ β where
  toFun x := x.1.getRight x.2
  invFun b := ⟨.inr b, Sum.isRight_inr⟩
  left_inv | ⟨.inr _b, _⟩ => rfl
  right_inv _b := rfl

end Equiv

namespace Finset
variable {α β : Type*} {s : Finset (α ⊕ β)} {a : α} {b : β}

def left (s : Finset (α ⊕ β)) : Finset α := (s.subtype _).map Equiv.sumIsLeft.toEmbedding
def right (s : Finset (α ⊕ β)) : Finset β := (s.subtype _).map Equiv.sumIsRight.toEmbedding

@[simp] lemma mem_left : a ∈ s.left ↔ .inl a ∈ s := by simp [left]
@[simp] lemma mem_right : b ∈ s.right ↔ .inr b ∈ s := by simp [right]

lemma disjSum_left_right (s : Finset (α ⊕ β)) : s.left.disjSum s.right = s := by
  ext (a | b) <;> simp

lemma card_left_add_card_right (s : Finset (α ⊕ β)) : #s.left + #s.right = #s := by
  simpa using congr(#$s.disjSum_left_right)

@[simp] lemma left_eq_univ [Fintype α] : s.left = univ ↔ univ.disjSum ∅ ⊆ s := by
  simp [eq_univ_iff_forall, subset_iff]

@[simp] lemma right_eq_empty [Fintype α] : s.right = ∅ ↔ s ⊆ univ.disjSum ∅ := by
  simp [eq_empty_iff_forall_not_mem, subset_iff]

end Finset

open Finset

lemma Finset.of_cardinality_between {α β : Type*} [Fintype α] [Fintype β] {n : ℕ}
    (hα : Fintype.card α < n) (hn : n ≤ Fintype.card α + Fintype.card β) :
    ∃ s : Finset β, Fintype.card α + #s = n ∧ s.Nonempty := by
  obtain ⟨s, hs, -, rfl⟩ : ∃ s : Finset (α ⊕ β), _ :=
    exists_subsuperset_card_eq (subset_univ <| univ.disjSum ∅) (by simpa using hα.le)
      (by simpa using hn)
  refine ⟨s.right, by simpa [left_eq_univ.2 hs] using s.card_left_add_card_right, ?_⟩
  simp only [nonempty_iff_ne_empty, ne_eq, right_eq_empty, disjSum_empty]
  exact fun h ↦ hα.not_le <| by simpa using card_le_card h

madvorak · 2025-01-22T15:44:58Z

Interesting.

YaelDillies · 2025-03-17T18:38:35Z

@madvorak, turns out my "new machinery that could belong in mathlib" was added to mathlib in #17014 by @b-mehta.

As a bonus, this lets us reduce imports. Also add the API that I independently came up with in #20433 (comment).

YaelDillies · 2025-03-17T19:21:19Z

		lemma of_cardinality_between_of_disjoint (hs : #s < n) (hn : n ≤ #s + #t) (hst : Disjoint s t) :
		∃ (x : Finset α) (hxs : Disjoint x s), #(x.disjUnion s hxs) = n ∧ Nonempty x := by

Conversation

madvorak commented Jan 3, 2025

Uh oh!

github-actions Bot commented Jan 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 61b2a51af5

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

alreadydone Jan 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

madvorak Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

madvorak Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone Jan 4, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jan 4, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies commented Jan 5, 2025

Uh oh!

madvorak commented Jan 6, 2025

Uh oh!

madvorak commented Jan 6, 2025

Uh oh!

YaelDillies commented Jan 6, 2025

Uh oh!

madvorak commented Jan 6, 2025

Uh oh!

madvorak commented Jan 13, 2025

Uh oh!

YaelDillies commented Jan 22, 2025

Uh oh!

madvorak commented Jan 22, 2025

Uh oh!

YaelDillies commented Mar 17, 2025

Uh oh!

YaelDillies commented Mar 17, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions Bot commented Jan 3, 2025 •

edited

Loading

alreadydone Jan 3, 2025 •

edited

Loading