@[simp]

theorem Partition.sUnion_eq {α : Type u_1} (P : Partition (Set α)) : ⋃₀ ↑P = P.supp

theorem Partition.nonempty_of_mem {α : Type u_1} {t : Set α} {P : Partition (Set α)} (ht : t ∈ P) : t.Nonempty

theorem Partition.empty_not_mem {α : Type u_1} {P : Partition (Set α)} : ∅ ∉ P

theorem Partition.subset_of_mem {α : Type u_1} {t : Set α} {P : Partition (Set α)} (ht : t ∈ P) : t ⊆ P.supp

theorem Partition.mem_supp_iff {α : Type u_1} {x : α} {P : Partition (Set α)} : x ∈ P.supp ↔ ∃ t ∈ P, x ∈ t

theorem Partition.eq_of_mem_inter {α : Type u_1} {x : α} {t u : Set α} {P : Partition (Set α)} (ht : t ∈ P) (hu : u ∈ P) (hx : x ∈ t ∩ u) : t = u

theorem Partition.eq_of_mem_of_mem {α : Type u_1} {x : α} {t u : Set α} {P : Partition (Set α)} (ht : t ∈ P) (hu : u ∈ P) (hxt : x ∈ t) (hxu : x ∈ u) : t = u

theorem Partition.exists_unique_of_mem_supp {α : Type u_1} {x : α} {P : Partition (Set α)} (hx : x ∈ P.supp) : ∃! t : Set α, t ∈ P ∧ x ∈ t

theorem Partition.mem_supp_iff_unique {α : Type u_1} {x : α} {P : Partition (Set α)} : x ∈ P.supp ↔ ∃! t : Set α, t ∈ P ∧ x ∈ t

theorem Partition.subset_sUnion_and_mem_iff_mem {α : Type u_1} {t : Set α} {S : Set (Set α)} {P : Partition (Set α)} (hSP : S ⊆ P.parts) : t ⊆ ⋃₀ S ∧ t ∈ P ↔ t ∈ S

@[simp]

theorem Partition.subset_sUnion_iff_mem {α : Type u_1} {t : Set α} {S : Set (Set α)} {P : Partition (Set α)} (ht : t ∈ P) (hSP : S ⊆ P.parts) : t ⊆ ⋃₀ S ↔ t ∈ S

theorem Partition.IsPartition.nonempty_not_mem {α : Type u_1} {t : Set α} {S : Set (Set α)} (hS : IsPartition S) (hx : t ∈ S) : t.Nonempty

theorem Partition.IsPartition.empty_not_mem {α : Type u_1} {S : Set (Set α)} (hS : IsPartition S) : ∅ ∉ S

theorem Partition.IsPartition.eq_of_mem_inter {α : Type u_1} {x : α} {t u : Set α} {S : Set (Set α)} (hS : IsPartition S) (ht : t ∈ S) (hu : u ∈ S) (hx : x ∈ t ∩ u) : t = u

theorem Partition.IsPartition.eq_of_mem_of_mem {α : Type u_1} {x : α} {t u : Set α} {S : Set (Set α)} (hS : IsPartition S) (ht : t ∈ S) (hu : u ∈ S) (hxt : x ∈ t) (hxu : x ∈ u) : t = u

def Partition.Rel {α : Type u_1} (P : Partition (Set α)) (a b : α) : Prop

Every partition of s : Set α induces a transitive, symmetric Binary relation on α whose equivalence classes are the parts of P. The relation is irreflexive outside s.

Equations

• P.Rel a b = ∃ t ∈ P, a ∈ t ∧ b ∈ t

theorem Partition.le_of_rel_le' {α : Type u_1} {P Q : Partition (Set α)} (h : P.Rel ≤ Q.Rel) : P ≤ Q

@[instance_reducible]

instance Partition.instFunLikeSetForallProp {α : Type u_1} : FunLike (Partition (Set α)) α (α → Prop)

Equations

• Partition.instFunLikeSetForallProp = { coe := Partition.Rel, coe_injective := ⋯ }

theorem Partition.Rel.exists {α : Type u_1} {x y : α} {P : Partition (Set α)} (h : P x y) : ∃ t ∈ P, x ∈ t ∧ y ∈ t

theorem Partition.Rel.forall {α : Type u_1} {x y : α} {T : Set α} {P : Partition (Set α)} (h : P x y) (ht : T ∈ P) : x ∈ T ↔ y ∈ T

theorem Partition.rel_of_mem_of_mem {α : Type u_1} {T : Set α} {a b : α} {P : Partition (Set α)} (ht : T ∈ P) (ha : a ∈ T) (hb : b ∈ T) : P a b

theorem Partition.rel_self_of_mem {α : Type u_1} {x : α} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) (hx : x ∈ T) : P x x

theorem Partition.rel_self_of_mem_supp {α : Type u_1} {x : α} {P : Partition (Set α)} (hx : x ∈ P.supp) : P x x

instance Partition.instSymmCoeSetForallProp {α : Type u_1} (P : Partition (Set α)) : Std.Symm ⇑P

instance Partition.instIsTransCoeSetForallProp {α : Type u_1} (P : Partition (Set α)) : IsTrans α ⇑P

theorem Partition.Rel.symm {α : Type u_1} {x y : α} {P : Partition (Set α)} (h : P x y) : P y x

theorem Partition.rel_comm {α : Type u_1} {x y : α} {P : Partition (Set α)} : P x y ↔ P y x

theorem Partition.Rel.trans {α : Type u_1} {x y z : α} {P : Partition (Set α)} (hxy : P x y) (hyz : P y z) : P x z

theorem Partition.Rel.left_mem {α : Type u_1} {x y : α} {P : Partition (Set α)} (h : P x y) : x ∈ P.supp

theorem Partition.Rel.right_mem {α : Type u_1} {x y : α} {P : Partition (Set α)} (h : P x y) : y ∈ P.supp

theorem Partition.rel_iff_exists {α : Type u_1} {x y : α} {P : Partition (Set α)} : P x y ↔ ∃ t ∈ P, x ∈ t ∧ y ∈ t

theorem Partition.rel_iff_right_mem_of_mem {α : Type u_1} {x y : α} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) (hx : x ∈ T) : P x y ↔ y ∈ T

theorem Partition.rel_iff_left_mem_of_mem {α : Type u_1} {x y : α} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) (hy : y ∈ T) : P x y ↔ x ∈ T

theorem Partition.rel_eq_exists {α : Type u_1} {P : Partition (Set α)} : ⇑P = fun (x y : α) => ∃ t ∈ P, x ∈ t ∧ y ∈ t

theorem Partition.mem_iff_forall_rel {α : Type u_1} {P : Partition (Set α)} {t : Set α} : t ∈ P ↔ ∃ (h : t.Nonempty), ∀ (x : α), P h.some x ↔ x ∈ t

theorem Partition.rel_self_iff_mem_supp {α : Type u_1} {x : α} {P : Partition (Set α)} : P x x ↔ x ∈ P.supp

theorem Partition.Rel.left_rfl {α : Type u_1} {x y : α} {P : Partition (Set α)} (h : P x y) : P x x

theorem Partition.Rel.right_rfl {α : Type u_1} {x y : α} {P : Partition (Set α)} (h : P x y) : P y y

@[simp]

theorem Partition.rel_bot {α : Type u_1} : ⇑⊥ = fun (x x_1 : α) => False

@[simp]

theorem Partition.rel_top {α : Type u_1} : ⇑⊤ = fun (x x_1 : α) => True

@[simp]

theorem Partition.domain_rel {α : Type u_1} {P : Partition (Set α)} : Relation.domain ⇑P = P.supp

@[simp]

theorem Partition.codomain_rel {α : Type u_1} {P : Partition (Set α)} : Relation.codomain ⇑P = P.supp

theorem Partition.rel_le_of_le {α : Type u_1} {P Q : Partition (Set α)} (h : P ≤ Q) : ⇑P ≤ ⇑Q

theorem Partition.le_of_rel_le {α : Type u_1} {P Q : Partition (Set α)} (h : ⇑P ≤ ⇑Q) : P ≤ Q

theorem Partition.rel_le_iff_le {α : Type u_1} {P Q : Partition (Set α)} : ⇑P ≤ ⇑Q ↔ P ≤ Q

theorem Partition.rel_inj {α : Type u_1} {P Q : Partition (Set α)} (h : ⇑P = ⇑Q) : P = Q

theorem Partition.rel_inj_iff {α : Type u_1} {P Q : Partition (Set α)} : ⇑P = ⇑Q ↔ P = Q

theorem Partition.rel_le_of_isInducedSubpartition {α : Type u_1} {P Q : Partition (Set α)} (h : P.isInducedSubpartition Q) : ⇑P ≤ ⇑Q

theorem Partition.rel_le_of_subset {α : Type u_1} {P Q : Partition (Set α)} (h : P.subset Q) : ⇑P ≤ ⇑Q

def Partition.ofRel {α : Type u_1} (r : α → α → Prop) [IsTrans α r] [Std.Symm r] : Partition (Set α)

A transitive, symmetric Binary relation r induces a partition of the set of elements on which it is reflexive.

Equations

• Partition.ofRel r = { parts := Relation.fibers r, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.ofRel_parts {α : Type u_1} (r : α → α → Prop) [IsTrans α r] [Std.Symm r] : (ofRel r).parts = Relation.fibers r

@[simp]

theorem Partition.ofRel_supp {α : Type u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] : (ofRel r).supp = Relation.domain r

@[simp]

theorem Partition.rel_ofRel_eq {α : Type u_1} {r : α → α → Prop} [IsTrans α r] [Std.Symm r] : ⇑(ofRel r) = r

theorem Partition.ofRel_rel_eq {α : Type u_1} (P : Partition (Set α)) : ofRel ⇑P = P

theorem Partition.fibers_rel_eq {α : Type u_1} {P : Partition (Set α)} : Relation.fibers ⇑P = P.parts

theorem Partition.eq_of_rel_iff_rel {α : Type u_1} {P P' : Partition (Set α)} (h : ∀ (x y : α), P x y ↔ P' x y) : P = P'

theorem Partition.eq_of_rel_iff_rel_iff {α : Type u_1} {P P' : Partition (Set α)} : P = P' ↔ ∀ (x y : α), P x y ↔ P' x y

def Partition.ofRel' {α : Type u_1} (r : α → α → Prop) : Partition (Set α)

Equations

• Partition.ofRel' r = Partition.ofRel (Relation.TransClosure (Relation.SymmClosure r))

@[simp]

theorem Partition.ofRel'_parts {α : Type u_1} (r : α → α → Prop) : (ofRel' r).parts = Relation.fibers (Relation.TransClosure (Relation.SymmClosure r))

@[simp]

theorem Partition.ofRel'_supp {α : Type u_1} {r : α → α → Prop} : (ofRel' r).supp = Relation.domain r ∪ Relation.codomain r

@[simp]

theorem Partition.rel_ofRel'_eq {α : Type u_1} {r : α → α → Prop} : ⇑(ofRel' r) = Relation.TransClosure (Relation.SymmClosure r)

theorem Partition.le_ofRel' {α : Type u_1} (r : α → α → Prop) : r ≤ ⇑(ofRel' r)

def Partition.partOf {α : Type u_1} (P : Partition (Set α)) (x : α) : Set α

The part containing a given element of the set being partitioned. If x ∉ s, then ∅.

Equations

• P.partOf x = Relation.fiber (⇑P) x

theorem Partition.partOf_subset_supp {α : Type u_1} {x : α} {P : Partition (Set α)} : P.partOf x ⊆ P.supp

theorem Partition.exists_partOf_iff_mem {α : Type u_1} {S : Set α} {P : Partition (Set α)} : S ∈ P ↔ ∃ x ∈ P.supp, P.partOf x = S

theorem Partition.partOf_mem {α : Type u_1} {x : α} {P : Partition (Set α)} (hx : x ∈ P.supp) : P.partOf x ∈ P

theorem Partition.partOf_eq_empty {α : Type u_1} {x : α} (P : Partition (Set α)) (hx : x ∉ P.supp) : P.partOf x = ∅

@[simp]

theorem Partition.partOf_ne_bot_iff {α : Type u_1} {x : α} {P : Partition (Set α)} : P.partOf x ≠ ⊥ ↔ x ∈ P.supp

@[simp]

theorem Partition.partOf_eq_empty_iff {α : Type u_1} {x : α} {P : Partition (Set α)} : P.partOf x = ∅ ↔ x ∉ P.supp

theorem Partition.mem_partOf {α : Type u_1} {x : α} {P : Partition (Set α)} (hx : x ∈ P.supp) : x ∈ P.partOf x

@[simp]

theorem Partition.mem_partOf_iff {α : Type u_1} {x y : α} {P : Partition (Set α)} : y ∈ P.partOf x ↔ P y x

theorem Partition.eq_partOf_of_mem {α : Type u_1} {x : α} {T : Set α} {P : Partition (Set α)} (ht : T ∈ P) (hxt : x ∈ T) : T = P.partOf x

theorem Partition.eq_partOf_iff_mem {α : Type u_1} {x : α} {T : Set α} {P : Partition (Set α)} (hxT : x ∈ T) : T = P.partOf x ↔ T ∈ P

theorem Partition.rel_iff_of_partOf_mem {α : Type u_1} {x y : α} {P Q : Partition (Set α)} (h : P.partOf x ∈ Q) : P x y ↔ Q x y

theorem Partition.partOf_mem_iff_rel_iff {α : Type u_1} {x : α} {P Q : Partition (Set α)} : P.partOf x ∈ Q ↔ x ∈ P.supp ∧ ∀ (y : α), P x y ↔ Q x y

@[simp]

theorem Partition.indiscrete_rel {α : Type u_1} {S : Set α} (hS : S ≠ ∅) : ⇑(indiscrete S hS) = fun (x y : α) => x ∈ S ∧ y ∈ S

@[simp]

theorem Partition.indiscrete'_rel {α : Type u_1} {S : Set α} : ⇑(indiscrete' S) = fun (x y : α) => x ∈ S ∧ y ∈ S

@[simp]

theorem Partition.induce_rel {α : Type u_1} (P : Partition (Set α)) {S : Set α} : ⇑(P.induce S) = fun (x y : α) => x ∈ S ∧ y ∈ S ∧ P x y

@[simp]

theorem Partition.induce_apply {α : Type u_1} {x y : α} (P : Partition (Set α)) {S : Set α} : (P.induce S) x y ↔ x ∈ S ∧ y ∈ S ∧ P x y

theorem Partition.isInducedSubpartition_iff_rel {α : Type u_1} (P Q : Partition (Set α)) : P.isInducedSubpartition Q ↔ (fun (x y : α) => x ∈ P.supp ∧ y ∈ P.supp ∧ Q x y) = ⇑P

theorem Partition.isInducedSubpartition.rel {α : Type u_1} {P Q : Partition (Set α)} (h : P.isInducedSubpartition Q) : ⇑P = fun (x y : α) => x ∈ P.supp ∧ y ∈ P.supp ∧ Q x y

theorem Partition.restrict_rel {α : Type u_1} (P : Partition (Set α)) {S : Set (Set α)} (hS : S ⊆ P.parts) : ⇑(P.restrict S hS) = fun (x y : α) => x ∈ ⋃₀ S ∧ P x y

@[simp]

theorem Partition.restrict_apply {α : Type u_1} {x y : α} (P : Partition (Set α)) {S : Set (Set α)} (hS : S ⊆ P.parts) : (P.restrict S hS) x y ↔ x ∈ ⋃₀ S ∧ P x y

theorem Partition.rel_of_restrict_rel {α : Type u_1} {x y : α} (P : Partition (Set α)) {S : Set (Set α)} (hS : S ⊆ P.parts) (hx : x ∈ ⋃₀ S) (hxy : P x y) : (P.restrict S hS) x y

@[simp]

theorem Partition.delete_rel {α : Type u_1} (P : Partition (Set α)) (S : Set (Set α)) : ⇑(P.delete S) = fun (x y : α) => ∃ t ∈ P.delete S, x ∈ t ∧ y ∈ t

theorem Partition.cover_rel {α : Type u_1} (P : Partition (Set α)) (S : Set α) : ⇑(P.cover S) = Relation.Domp ⇑P ⇑(P.induce S)

@[simp]

theorem Partition.cover_rel_of_left_mem {α : Type u_1} {x y : α} {S : Set α} (P : Partition (Set α)) (hx : x ∈ S) : (P.cover S) x y ↔ P x y

@[simp]

theorem Partition.cover_rel_of_right_mem {α : Type u_1} {x y : α} {S : Set α} (P : Partition (Set α)) (hy : y ∈ S) : (P.cover S) x y ↔ P x y

theorem Partition.subset_cover_supp {α : Type u_1} {S : Set α} {P : Partition (Set α)} (h : S ⊆ P.supp) : S ⊆ (P.cover S).supp

theorem Partition.rel_of_subset_mem {α : Type u_1} {x y : α} {P Q : Partition (Set α)} (hPQ : P.subset Q) (hx : x ∈ P.supp) (hxy : Q x y) : P x y

theorem Partition.subset_iff_rel {α : Type u_1} {P Q : Partition (Set α)} : P.subset Q ↔ ∀ ⦃x y : α⦄, x ∈ P.supp → (P x y ↔ Q x y)

theorem Partition.agree_iff_rel {α : Type u_1} {P Q : Partition (Set α)} : P.Agree Q ↔ ∀ (x y : α), x ∈ P.supp → x ∈ Q.supp → (P x y ↔ Q x y)

theorem Partition.Agree.rel_of_left_of_mem {α : Type u_1} {x y : α} {P Q : Partition (Set α)} (h : P.Agree Q) (hx : x ∈ Q.supp) (hxy : P x y) : Q x y

theorem Partition.Agree.rel_of_right_of_mem {α : Type u_1} {x y : α} {P Q : Partition (Set α)} (h : P.Agree Q) (hy : x ∈ P.supp) (hxy : Q x y) : P x y

theorem Partition.Agree.trans_left {α : Type u_1} {a b c : α} {P Q : Partition (Set α)} (h : P.Agree Q) (hab : P a b) (hbc : Q b c) : P a c

theorem Partition.Agree.trans_right {α : Type u_1} {a b c : α} {P Q : Partition (Set α)} (h : P.Agree Q) (hab : P a b) (hbc : Q b c) : Q a c

theorem Partition.Agree.sup_rel_trans {α : Type u_1} {a b c : α} {P Q : Partition (Set α)} (h : P.Agree Q) (hab : (⇑P ⊔ ⇑Q) a b) (hbc : (⇑P ⊔ ⇑Q) b c) : (⇑P ⊔ ⇑Q) a c

theorem Partition.inf_rel_trans {α : Type u_1} {a b c : α} {P Q : Partition (Set α)} (hab : (⇑P ⊓ ⇑Q) a b) (hbc : (⇑P ⊓ ⇑Q) b c) : (⇑P ⊓ ⇑Q) a c

def Partition.discrete {α : Type u_5} (S : Set α) : Partition (Set α)

The discrete partition

Equations

• Partition.discrete S = { parts := singleton '' S, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.discrete_parts {α : Type u_5} (S : Set α) : (Partition.discrete S).parts = singleton '' S

@[simp]

theorem Partition.supp_discrete {α : Type u_5} (S : Set α) : (Partition.discrete S).supp = S

@[simp]

theorem Partition.mem_discrete_iff {α : Type u_5} {S T : Set α} : T ∈ Partition.discrete S ↔ ∃ a ∈ S, {a} = T

theorem Partition.mem_discrete_of_mem_supp {α : Type u_5} {S : Set α} {x : α} (h : x ∈ S) : {x} ∈ Partition.discrete S

theorem Partition.rel_discrete_eq' {α : Type u_5} {S : Set α} : ⇑(Partition.discrete S) = fun (a b : α) => a = b ∧ b ∈ S

@[simp]

theorem Partition.rel_discrete_eq {α : Type u_5} {S : Set α} : ⇑(Partition.discrete S) = fun (a b : α) => a = b ∧ a ∈ S

@[simp]

theorem Partition.rel_discrete_iff {α : Type u_5} {S : Set α} {a b : α} : (Partition.discrete S) a b ↔ a = b ∧ a ∈ S

theorem Partition.eq_of_rel_of_left_singleton_mem {α : Type u_5} {a b : α} {P : Partition (Set α)} (hab : P a b) (ha : {a} ∈ P) : a = b

theorem Partition.eq_of_rel_of_right_singleton_mem {α : Type u_5} {a b : α} {P : Partition (Set α)} (hab : P a b) (hb : {b} ∈ P) : a = b

@[simp]

theorem Partition.discrete_atomic {α : Type u_5} (S : Set α) : (Partition.discrete S).Atomic

theorem Partition.Atomic.exists_singleton_of_mem {α : Type u_5} {P : Partition (Set α)} (hP : P.Atomic) {t : Set α} (htP : t ∈ P) : ∃ (a : α), t = {a}

theorem Partition.atomic_iff_eq_discrete {α : Type u_5} (P : Partition (Set α)) : P.Atomic ↔ P = Partition.discrete P.supp

@[simp]

theorem Partition.mem_atomic_iff {α : Type u_5} {S : Set α} {P : Partition (Set α)} (hP : P.Atomic) : S ∈ P ↔ ∃ a ∈ P.supp, {a} = S

theorem Partition.eq_discrete_iff {α : Type u_5} {S : Set α} {P : Partition (Set α)} : P = Partition.discrete S ↔ P.Atomic ∧ P.supp = S

theorem Partition.eq_discrete_of {α : Type u_5} {S : Set α} {P : Partition (Set α)} (hP : P.Atomic) (hS : P.supp = S) : P = Partition.discrete S

theorem Partition.discrete_le_of_supp_eq {α : Type u_5} (P : Partition (Set α)) : Partition.discrete P.supp ≤ P

theorem Partition.atomic_iff_rel_le_eq {α : Type u_5} (P : Partition (Set α)) : P.Atomic ↔ ⇑P ≤ Eq

theorem Partition.Atomic.eq_of_rel {α : Type u_5} {a b : α} {P : Partition (Set α)} (hP : P.Atomic) (hab : P a b) : a = b

theorem Partition.Atomic.rel_eq {α : Type u_5} {P : Partition (Set α)} (hP : P.Atomic) : ⇑P = fun (a b : α) => a = b ∧ a ∈ P.supp

theorem Partition.discrete_of_le_discrete {α : Type u_5} {S : Set α} {P : Partition (Set α)} (hS : P ≤ Partition.discrete S) : P = Partition.discrete P.supp

theorem Partition.discrete_subset_discrete_of_subset {α : Type u_5} {S T : Set α} (hST : S ⊆ T) : (Partition.discrete S).subset (Partition.discrete T)

@[simp]

theorem Partition.discrete_subset_discrete_iff {α : Type u_5} {S T : Set α} : (Partition.discrete S).subset (Partition.discrete T) ↔ S ⊆ T

theorem Partition.discrete_mono {α : Type u_5} {S T : Set α} (hST : S ⊆ T) : Partition.discrete S ≤ Partition.discrete T

theorem Partition.discrete_subset_iff_rel {α : Type u_5} {S : Set α} {P : Partition (Set α)} : (Partition.discrete S).subset P ↔ ∀ (x y : α), x ∈ S → (x = y ↔ P x y)

@[simp]

theorem Partition.discrete_empty {α : Type u_5} : Partition.discrete ∅ = ⊥

theorem Partition.supp_singleton_iff {α : Type u_5} {a : α} {P : Partition (Set α)} (hP : P.supp = {a}) : P = Partition.discrete {a}

theorem Partition.atomic_of_supp_singleton {α : Type u_5} {a : α} {P : Partition (Set α)} (hP : P.supp = {a}) : P.Atomic

@[simp]

theorem Partition.discrete_le_iff {α : Type u_5} {S : Set α} {P : Partition (Set α)} : Partition.discrete S ≤ P ↔ S ⊆ P.supp

@[simp]

theorem Partition.discrete_isInducedSubpartition_iff {α : Type u_5} {S : Set α} {Q : Partition (Set α)} : (Partition.discrete S).isInducedSubpartition Q ↔ S ⊆ Q.supp ∧ (Q.induce S).Atomic

@[simp]

theorem Partition.agree_of_atomic {α : Type u_5} {P Q : Partition (Set α)} (hP : P.Atomic) (hQ : Q.Atomic) : P.Agree Q

def Partition.flatten {α : Type u_1} [Order.Frame α] (P : Partition (Set α)) {Q : Partition α} (h : P.supp = Q.parts) : Partition α

Equations

• P.flatten h = { parts := sSup '' P.parts, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.flatten_parts {α : Type u_1} [Order.Frame α] {Q : Partition α} (P : Partition (Set α)) (h : P.supp = Q.parts) : (P.flatten h).parts = sSup '' P.parts

@[simp]

theorem Partition.flatten_supp {α : Type u_1} [Order.Frame α] {Q : Partition α} (P : Partition (Set α)) (h : P.supp = Q.parts) : (P.flatten h).supp = Q.supp

theorem Partition.le_flatten {α : Type u_1} [Order.Frame α] {Q : Partition α} (P : Partition (Set α)) (h : P.supp = Q.parts) : Q ≤ P.flatten h