[Merged by Bors] - chore: Split data.set.pairwise
#3117
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
GitHub Actions
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,121 @@ | ||
| /- | ||
| Copyright (c) 2017 Johannes Hölzl. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Johannes Hölzl | ||
|
|
||
| ! This file was ported from Lean 3 source module data.set.pairwise.lattice | ||
| ! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0 | ||
| ! Please do not edit these lines, except to modify the commit id | ||
| ! if you have ported upstream changes. | ||
| -/ | ||
| import Mathlib.Data.Set.Lattice | ||
| import Mathlib.Data.Set.Pairwise.Basic | ||
|
|
||
| /-! | ||
| # Relations holding pairwise | ||
| In this file we prove many facts about `pairwise` and the set lattice. | ||
| -/ | ||
|
|
||
| open Set Function | ||
|
|
||
| variable {α β γ ι ι' : Type _} {r p q : α → α → Prop} {s t : Set ι} | ||
|
|
||
| namespace Set | ||
| variable {f g : ι → α} | ||
|
|
||
| theorem pairwise_unionᵢ {f : ι → Set α} (h : Directed (· ⊆ ·) f) : | ||
| (⋃ n, f n).Pairwise r ↔ ∀ n, (f n).Pairwise r := by | ||
| constructor | ||
| · intro H n | ||
| exact Pairwise.mono (subset_unionᵢ _ _) H | ||
| · intro H i hi j hj hij | ||
| rcases mem_unionᵢ.1 hi with ⟨m, hm⟩ | ||
| rcases mem_unionᵢ.1 hj with ⟨n, hn⟩ | ||
| rcases h m n with ⟨p, mp, np⟩ | ||
| exact H p (mp hm) (np hn) hij | ||
| #align set.pairwise_Union Set.pairwise_unionᵢ | ||
|
|
||
| theorem pairwise_unionₛ {r : α → α → Prop} {s : Set (Set α)} (h : DirectedOn (· ⊆ ·) s) : | ||
| (⋃₀s).Pairwise r ↔ ∀ a ∈ s, Set.Pairwise a r := by | ||
| rw [unionₛ_eq_unionᵢ, pairwise_unionᵢ h.directed_val, SetCoe.forall] | ||
| #align set.pairwise_sUnion Set.pairwise_unionₛ | ||
|
|
||
| section PartialOrder | ||
| variable [PartialOrder α] [OrderBot α] | ||
|
|
||
| theorem pairwiseDisjoint_unionᵢ {g : ι' → Set ι} (h : Directed (· ⊆ ·) g) : | ||
| (⋃ n, g n).PairwiseDisjoint f ↔ ∀ ⦃n⦄, (g n).PairwiseDisjoint f := | ||
| pairwise_unionᵢ h | ||
| #align set.pairwise_disjoint_Union Set.pairwiseDisjoint_unionᵢ | ||
|
|
||
| theorem pairwiseDisjoint_unionₛ {s : Set (Set ι)} (h : DirectedOn (· ⊆ ·) s) : | ||
| (⋃₀s).PairwiseDisjoint f ↔ ∀ ⦃a⦄, a ∈ s → PairwiseDisjoint a f := | ||
| pairwise_unionₛ h | ||
| #align set.pairwise_disjoint_sUnion Set.pairwiseDisjoint_unionₛ | ||
|
|
||
| end PartialOrder | ||
|
|
||
| section CompleteLattice | ||
| variable [CompleteLattice α] | ||
|
|
||
| /-- Bind operation for `Set.PairwiseDisjoint`. If you want to only consider finsets of indices, you | ||
| can use `Set.PairwiseDisjoint.bunionᵢ_finset`. -/ | ||
| theorem PairwiseDisjoint.bunionᵢ {s : Set ι'} {g : ι' → Set ι} | ||
| (hs : s.PairwiseDisjoint fun i' : ι' => ⨆ i ∈ g i', f i) | ||
| (hg : ∀ i ∈ s, (g i).PairwiseDisjoint f) : (⋃ i ∈ s, g i).PairwiseDisjoint f := by | ||
| rintro a ha b hb hab | ||
| simp_rw [mem_unionᵢ] at ha hb | ||
| obtain ⟨c, hc, ha⟩ := ha | ||
| obtain ⟨d, hd, hb⟩ := hb | ||
| obtain hcd | hcd := eq_or_ne (g c) (g d) | ||
| · exact hg d hd (hcd.subst ha) hb hab | ||
| -- Porting note: the elaborator couldn't figure out `f` here. | ||
| · exact (hs hc hd <| ne_of_apply_ne _ hcd).mono | ||
| (le_supᵢ₂ (f := fun i (_ : i ∈ g c) => f i) a ha) | ||
| (le_supᵢ₂ (f := fun i (_ : i ∈ g d) => f i) b hb) | ||
| #align set.pairwise_disjoint.bUnion Set.PairwiseDisjoint.bunionᵢ | ||
|
|
||
| end CompleteLattice | ||
|
|
||
| theorem bunionᵢ_diff_bunionᵢ_eq {s t : Set ι} {f : ι → Set α} (h : (s ∪ t).PairwiseDisjoint f) : | ||
| ((⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i) = ⋃ i ∈ s \ t, f i := by | ||
| refine' | ||
| (bunionᵢ_diff_bunionᵢ_subset f s t).antisymm | ||
| (unionᵢ₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_bunionᵢ hi.1 ha, _⟩) | ||
| rw [mem_unionᵢ₂]; rintro ⟨j, hj, haj⟩ | ||
| exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩ | ||
| #align set.bUnion_diff_bUnion_eq Set.bunionᵢ_diff_bunionᵢ_eq | ||
|
|
||
| /-- Equivalence between a disjoint bounded union and a dependent sum. -/ | ||
| noncomputable def bunionᵢEqSigmaOfDisjoint {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) : | ||
| (⋃ i ∈ s, f i) ≃ Σ i : s, f i := | ||
| (Equiv.setCongr (bunionᵢ_eq_unionᵢ _ _)).trans <| | ||
| unionEqSigmaOfDisjoint fun ⟨_i, hi⟩ ⟨_j, hj⟩ ne => (h hi hj) fun eq => ne <| Subtype.eq eq | ||
| #align set.bUnion_eq_sigma_of_disjoint Set.bunionᵢEqSigmaOfDisjoint | ||
|
|
||
| end Set | ||
|
|
||
| section | ||
| variable {f : ι → Set α} {s t : Set ι} | ||
|
|
||
| theorem Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ (h₀ : (s ∪ t).PairwiseDisjoint f) | ||
| (h₁ : ∀ i ∈ s, (f i).Nonempty) (h : (⋃ i ∈ s, f i) ⊆ ⋃ i ∈ t, f i) : s ⊆ t := by | ||
| rintro i hi | ||
| obtain ⟨a, hai⟩ := h₁ i hi | ||
| obtain ⟨j, hj, haj⟩ := mem_unionᵢ₂.1 (h <| mem_unionᵢ₂_of_mem hi hai) | ||
| rwa [h₀.eq (subset_union_left _ _ hi) (subset_union_right _ _ hj) | ||
| (not_disjoint_iff.2 ⟨a, hai, haj⟩)] | ||
| #align set.pairwise_disjoint.subset_of_bUnion_subset_bUnion Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ | ||
|
|
||
| theorem Pairwise.subset_of_bunionᵢ_subset_bunionᵢ (h₀ : Pairwise (Disjoint on f)) | ||
| (h₁ : ∀ i ∈ s, (f i).Nonempty) (h : (⋃ i ∈ s, f i) ⊆ ⋃ i ∈ t, f i) : s ⊆ t := | ||
| Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ (h₀.set_pairwise _) h₁ h | ||
| #align pairwise.subset_of_bUnion_subset_bUnion Pairwise.subset_of_bunionᵢ_subset_bunionᵢ | ||
|
|
||
| theorem Pairwise.bunionᵢ_injective (h₀ : Pairwise (Disjoint on f)) (h₁ : ∀ i, (f i).Nonempty) : | ||
| Injective fun s : Set ι => ⋃ i ∈ s, f i := fun _ _ h => | ||
| ((h₀.subset_of_bunionᵢ_subset_bunionᵢ fun _ _ => h₁ _) <| h.subset).antisymm <| | ||
| (h₀.subset_of_bunionᵢ_subset_bunionᵢ fun _ _ => h₁ _) <| h.superset | ||
| #align pairwise.bUnion_injective Pairwise.bunionᵢ_injective | ||
|
|
||
| end |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we understand why this import is needed here but not in mathlib?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We should try removing it again with the intermediate backport now in place (once we have a cache)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, it seems that mathlib3 gets it from these tactic imports: