Placing an order on a finite set

Stream: mathlib4

[Connor Gordon]

(For the full context of this question, you can check out this conversation.)

I currently have a function B : α → Set β, and would like to create another function B' : α → Set β such that the outputs of B' are pairwise disjoint. Infrastructure to do this for functions of the form ℕ → Set β exists in Docs#Disjointed, but I have been unsuccessful in finding an implementation more generally.

For my intended use specifically, I only care about disjointedness within a single specific F : Finset α rather than all of α, but even this is eluding me. Part of me would like to use F.toList and attempt to reason from there, but my attempts thus far have been unsuccessful. Any ideas on how I could do this?

[Kevin Buzzard]

Set is a mathlib thing, not a core Lean 4 thing, so this question is in the wrong stream -- can someone move it to #mathlib4 ?

I'm assuming that you want the union over B' to be equal to the union over B? Either that or something else is missing from your question (the answer to the question right now is "let B' x be the empty set for all x").

In general why not just well-order alpha and define $B'(x)$ to be the things which are in $B(x)$ but not in $B(y)$ for any $y<x$?

[Connor Gordon]

Ah, apologies for the wrong stream. I'm still somewhat new to messaging on Zulip, and I'll keep it in mind going forward.

And also allow me to clarify what I mean. I have a function that is really defined from F → Set β, for a specific F : Finset α, but was recommended to define the function from α → Set βin its entirety and ignore the part outside of F. Yes, I do want to preserve the union, but specifically with respect to the set F (same with making things disjoint; I really only care about behavior on F).

As for well-ordering, I would love to be able to do that, but I genuinely have no idea how (and again, really would need to specifically well-order F).

Hopefully that addresses everything, apologies for the lack of specificity in my original post.

[Kevin Buzzard]

Oh OK. I should think this would work then:

import Mathlib

variable {α β : Type*} (B : α → Set β) (F : Finset α)

-- use axiom of choice to well-order α
noncomputable instance : LinearOrder α := IsWellOrder.linearOrder WellOrderingRel

-- B' is a function of B and F
def B' (a : α) : Set β := {x : β | x ∈ B a ∧ ∀ a' < a, a' ∈ F → x ∉ B a'}

[Notification Bot]

This topic was moved here from #lean4 > Placing an order on a finite set by Jireh Loreaux.

[Kevin Buzzard]

(thanks Jireh). This function B' B F should (if I got the maths right) have the property that the union over a in F of B(a) equals the union over a in F of B'(a), and the B'(a) for a in F are disjoint. Is that what you're after?

[Connor Gordon]

Yes it is, thank you so much! I'll give it a go and see if it works for me!

[Kevin Buzzard]

My effort

I didn't leave comments but I didn't try any golfing so hopefully the code is not too hard to read.

import Mathlib

variable {α β : Type*} (B : α → Set β) (F : Finset α)

-- use axiom of choice to well-order α
noncomputable instance : LinearOrder α := IsWellOrder.linearOrder WellOrderingRel

-- B' is a function of B and F
abbrev B' (a : α) : Set β := {x : β | x ∈ B a ∧ ∀ a' < a, a' ∈ F → x ∉ B a'}

lemma lemma1 (a : α) : B' B F a ⊆ B a := by simp [B']

example : ⋃ a ∈ F, B a = ⋃ a ∈ F, B' B F a := by
  apply Set.Subset.antisymm
  · rw [Set.iUnion_subset_iff]
    intro i b hb
    rw [Set.mem_iUnion] at hb ⊢
    rcases hb with ⟨h1, h2⟩
    classical
    let S : Finset α := F.filter (fun a ↦ b ∈ B a)
    have hiS : i ∈ S := by
      rw [Finset.mem_filter]
      exact ⟨h1, h2⟩
    have hS' : S.Nonempty := ⟨i, hiS⟩
    let j : α := Finset.min' S hS'
    have hj2 : j ∈ S := S.min'_mem hS'
    rw [Finset.mem_filter] at hj2
    rcases hj2 with ⟨hjF, hBj⟩
    use j
    rw [Set.mem_iUnion]
    use hjF
    refine ⟨hBj, fun a' ha'j ha'F hb ↦ ?_⟩
    have ha'S : a' ∈ S := by
      rw [Finset.mem_filter]
      exact ⟨ha'F, hb⟩
    have : j ≤ a' := S.min'_le a' ha'S
    exact not_lt.2 this ha'j
  · apply Set.iUnion_mono (fun i ↦ ?_)
    apply Set.iUnion_mono (fun _ ↦ ?_)
    apply lemma1

lemma aux {a₁ a₂ : α} (h₁ : a₁ ∈ F) (h : a₁ < a₂) :
    Disjoint (B' B F a₁) (B' B F a₂) := by
  rw [Set.disjoint_left]
  rintro b ⟨h1, -⟩ ⟨-, h2⟩
  apply h2 a₁ h h₁ h1

example (a₁ a₂ : α) (h₁ : a₁ ∈ F) (h₂ : a₂ ∈ F) (h : a₁ ≠ a₂) : Disjoint (B' B F a₁) (B' B F a₂) := by
  rcases lt_trichotomy a₁ a₂ with (h' | rfl | h')
  · exact aux B F h₁ h'
  · contradiction
  · rw [disjoint_comm]
    exact aux B F h₂ h'

[Connor Gordon]

This works, thanks!