def Set.IsPartition {α : Type u_1} {ι : Type u_3} (x : ι → Set α) : Prop

Equations

• Set.IsPartition x = (Set.IsCovering x ∧ Set.Disjoint x)

theorem Set.eq_of_mem_disjoint {α : Type u_1} {ι : Type u_3} {a : α} {i j : ι} {x : ι → Set α} (h : Set.Disjoint x) (h' : a ∈ x i) (h'' : a ∈ x j) : i = j

theorem Set.IsPartition.eq_of_mem {α : Type u_1} {ι : Type u_3} {a : α} {i j : ι} {x : ι → Set α} (h : Set.IsPartition x) (h' : a ∈ x i) (h'' : a ∈ x j) : i = j

theorem Set.isPartition_iff {α : Type u_1} {ι : Type u_3} {x : ι → Set α} : Set.IsPartition x ↔ ∀ (a : α), ∃! i : ι, a ∈ x i

theorem Set.IsPartition.preimage {α : Type u_1} {β : Type u_2} {ι : Type u_3} {f : α → β} {y : ι → Set β} (h : Set.IsPartition y) : Set.IsPartition (Set.preimage f ∘ y)

theorem Set.IsPartition.image_bij {α : Type u_1} {β : Type u_2} {ι : Type u_3} {x : ι → Set α} {f : α → β} (h : Set.IsPartition x) (h' : Function.Bijective f) : Set.IsPartition (Set.image f ∘ x)

theorem Set.IsPartition.inj_of_nonempty {α : Type u_1} {ι : Type u_3} {x : ι → Set α} (h : Set.IsPartition x) (h' : ∀ (i : ι), (x i).Nonempty) : Function.Injective x

theorem Set.IsPartition.subset_of_finerThan {α : Type u_1} {ι : Type u_3} {ι' : Type u_4} {x : ι → Set α} {x' : ι' → Set α} (h : Set.IsPartition x) (h' : Set.IsPartition x') (hne : ∀ (i : ι), (x i).Nonempty) (hne' : ∀ (i' : ι'), (x' i').Nonempty) (h'' : Set.FinerThan x x') (i' : ι') : ∃ (i : ι), x i ⊆ x' i'

@[simp]

theorem Set.IsPartition.glue_agrees {α : Type u_1} {ι : Type u_3} {a : α} {i : ι} {x : ι → Set α} {β : α → Type u_6} (h : Set.IsPartition x) {f : (i : ι) → (a : ↥(x i)) → β a.val} (h' : a ∈ x i) : ⋯.glue f a = f i ⟨a, h'⟩

theorem Set.singleton_partition {α : Type u_1} : Set.IsPartition fun (x : α) => {x}

structure Set.Partition (α : Type u_6) : Type u_6

• subsets : Set (Set α)
• isPartition' : Set.IsPartition fun (x : ↥self.subsets) => x.val
• empty_not_included : ¬∅ ∈ self.subsets

theorem Set.Partition.eq_iff {α : Type u_1} {p q : Set.Partition α} : p = q ↔ p.subsets = q.subsets

theorem Set.Partition.eq_of {α : Type u_1} {p q : Set.Partition α} : p.subsets = q.subsets → p = q

def Set.Partition.partition {α : Type u_1} (p : Set.Partition α) : ↥p.subsets → Set α

Equations

• p.partition = Subtype.val

@[simp]

theorem Set.Partition.isPartition {α : Type u_1} (p : Set.Partition α) : Set.IsPartition p.partition

@[simp]

theorem Set.partition.val_partition {α : Type u_1} {p : Set.Partition α} {q : Set α} {h : q ∈ p.subsets} : p.partition ⟨q, h⟩ = q

theorem Set.IsPartition.equivalent_partition {α : Type u_1} {ι : Type u_3} {x : ι → Set α} (h : Set.IsPartition x) (ne : ∀ (i : ι), (x i).Nonempty) : ∃ (p : Set.Partition α), Set.FinerThan p.partition x ∧ Set.FinerThan x p.partition

theorem Set.Partition.all_nonempty {α : Type u_1} (p : Set.Partition α) {a : Set α} (h' : a ∈ p.subsets) : a.Nonempty