structure Set.IndexedPartition {α : Type u_2} (s : Set α) (ι : Type u_3) : Type (max u_2 u_3)

• toFun : ι → Set α
• pairwise_disjoint' : Pairwise (Function.onFun Disjoint self.toFun)
• iUnion_eq' : ⋃ (i : ι), self.toFun i = s

@[instance_reducible]

instance Set.IndexedPartition.instFunLike {α : Type u_1} {s : Set α} {ι : Type u_2} : FunLike (s.IndexedPartition ι) ι (Set α)

Equations

• Set.IndexedPartition.instFunLike = { coe := Set.IndexedPartition.toFun, coe_injective := ⋯ }

@[simp]

theorem Set.IndexedPartition.toFun_eq_coe {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) : P.toFun = ⇑P

@[simp]

theorem Set.IndexedPartition.mk_apply {α : Type u_1} {s : Set α} {ι : Type u_2} (f : ι → Set α) (dj : Pairwise (Function.onFun Disjoint f)) (hu : ⋃ (i : ι), f i = s) (i : ι) : { toFun := f, pairwise_disjoint' := dj, iUnion_eq' := hu } i = f i

theorem Set.IndexedPartition.ext {α : Type u_1} {s : Set α} {ι : Type u_2} {P Q : s.IndexedPartition ι} (h : ∀ (i : ι), P i = Q i) : P = Q

theorem Set.IndexedPartition.ext_iff {α : Type u_1} {s : Set α} {ι : Type u_2} {P Q : s.IndexedPartition ι} : P = Q ↔ ∀ (i : ι), P i = Q i

theorem Set.IndexedPartition.pairwise_disjoint {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) : Pairwise (Function.onFun Disjoint ⇑P)

theorem Set.IndexedPartition.disjoint {α : Type u_1} {s : Set α} {ι : Type u_2} {i j : ι} (P : s.IndexedPartition ι) (hij : i ≠ j) : Disjoint (P i) (P j)

theorem Set.IndexedPartition.iUnion_eq {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) : ⋃ (i : ι), P i = s

@[simp]

theorem Set.IndexedPartition.subset {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) {i : ι} : P i ⊆ s

@[simp]

theorem Set.IndexedPartition.inter_ground_left {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (i : ι) : P i ∩ s = P i

@[simp]

theorem Set.IndexedPartition.inter_ground_right {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (i : ι) : s ∩ P i = P i

theorem Set.IndexedPartition.exists_mem {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) {a : α} (ha : a ∈ s) : ∃ (i : ι), a ∈ P i

theorem Set.IndexedPartition.eq_of_mem_of_mem {α : Type u_1} {s : Set α} {ι : Type u_2} {i j : ι} {P : s.IndexedPartition ι} {a : α} (hi : a ∈ P i) (hj : a ∈ P j) : i = j

theorem Set.IndexedPartition.existsUnique_mem {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) {a : α} (ha : a ∈ s) : ∃! i : ι, a ∈ P i

theorem Set.IndexedPartition.single_eq_diff_iUnion {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (i : ι) : P i = s \ ⋃ (j : ι), ⋃ (_ : j ≠ i), P j

theorem Set.IndexedPartition.ext' {α : Type u_1} {s : Set α} {ι : Type u_2} {P Q : s.IndexedPartition ι} {j : ι} (h : ∀ (i : ι), i ≠ j → P i = Q i) : P = Q

def Set.IndexedPartition.ofSubtypeFun {α : Type u_1} {s : Set α} {ι : Type u_2} (f : ↑s → ι) : s.IndexedPartition ι

Reconstruct a partition from an indexing function on a subtype.

Equations

• Set.IndexedPartition.ofSubtypeFun f = { toFun := fun (i : ι) => Subtype.val '' f ⁻¹' {i}, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.ofSubtypeFun_apply {α : Type u_1} {s : Set α} {ι : Type u_2} (f : ↑s → ι) (i : ι) : (ofSubtypeFun f) i = Subtype.val '' f ⁻¹' {i}

noncomputable def Set.IndexedPartition.equivSubtype {α : Type u_1} (s : Set α) (ι : Type u_4) : s.IndexedPartition ι ≃ (↑s → ι)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Set.IndexedPartition.equivPFun {α : Type u_1} (ι : Type u_4) : (s : Set α) × s.IndexedPartition ι ≃ (α →. ι)

Equations

• One or more equations did not get rendered due to their size.

def Set.IndexedPartition.copy {α : Type u_1} {s t : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (h_eq : s = t) : t.IndexedPartition ι

Transfer a partition across a set equality.

Equations

• P.copy h_eq = { toFun := P.toFun, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.copy_apply {α : Type u_1} {s t : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (h_eq : s = t) (i : ι) : (P.copy h_eq) i = P i

def Set.IndexedPartition.copyEquiv {α : Type u_1} {s t : Set α} {ι : Type u_2} (h_eq : s = t) : s.IndexedPartition ι ≃ t.IndexedPartition ι

Equations

• Set.IndexedPartition.copyEquiv h_eq = { toFun := fun (P : s.IndexedPartition ι) => P.copy h_eq, invFun := fun (P : t.IndexedPartition ι) => P.copy ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Set.IndexedPartition.copyEquiv_symm_apply {α : Type u_1} {s t : Set α} {ι : Type u_2} (h_eq : s = t) (P : t.IndexedPartition ι) : (IndexedPartition.copyEquiv h_eq).symm P = P.copy ⋯

@[simp]

theorem Set.IndexedPartition.copyEquiv_apply {α : Type u_1} {s t : Set α} {ι : Type u_2} (h_eq : s = t) (P : s.IndexedPartition ι) : (IndexedPartition.copyEquiv h_eq) P = P.copy h_eq

def Set.IndexedPartition.induce {α : Type u_1} {s t : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (hts : t ⊆ s) : t.IndexedPartition ι

Intersect a partition with a smaller set

Equations

• P.induce hts = { toFun := fun (i : ι) => P i ∩ t, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.induce_apply {α : Type u_1} {s t : Set α} {ι : Type u_2} {P : s.IndexedPartition ι} {hts : t ⊆ s} {i : ι} : (P.induce hts) i = P i ∩ t

@[simp]

theorem Set.IndexedPartition.induce_induce {α : Type u_1} {r s t : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (hts : t ⊆ s) (hrt : r ⊆ t) : (P.induce hts).induce hrt = P.induce ⋯

@[simp]

theorem Set.IndexedPartition.induce_rfl {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (h : s ⊆ s := ⋯) : P.induce h = P

def Set.IndexedPartition.LE {α : Type u_1} {s t : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (Q : t.IndexedPartition ι) : Prop

IndexedPartition.LE P Q, written P ≤ Q, means that every cell of P is contained in the corresponding cell of Q.

Equations

• P.LE Q = ∀ (i : ι), P i ⊆ Q i

def Set.IndexedPartition.«term_≤_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Set.IndexedPartition.le_iff {α : Type u_1} {s t : Set α} {ι : Type u_2} {P : s.IndexedPartition ι} {Q : t.IndexedPartition ι} : P.LE Q ↔ ∀ (i : ι), P i ⊆ Q i

theorem Set.IndexedPartition.LE.trans {α : Type u_1} {r s t : Set α} {ι : Type u_2} {P : r.IndexedPartition ι} {Q : s.IndexedPartition ι} (R : t.IndexedPartition ι) (hPQ : P.LE Q) (hQR : Q.LE R) : P.LE R

theorem Set.IndexedPartition.LE.subset {α : Type u_1} {s t : Set α} {ι : Type u_2} {P : s.IndexedPartition ι} {Q : t.IndexedPartition ι} (hPQ : P.LE Q) : s ⊆ t

theorem Set.IndexedPartition.LE.disjoint_of_ne {α : Type u_1} {s t : Set α} {ι : Type u_2} {i j : ι} {P : s.IndexedPartition ι} {Q : t.IndexedPartition ι} (hPQ : P.LE Q) (hij : i ≠ j) : Disjoint (P i) (Q j)

theorem Set.IndexedPartition.LE.eq_induce {α : Type u_1} {s t : Set α} {ι : Type u_2} {P : s.IndexedPartition ι} {Q : t.IndexedPartition ι} (hPQ : P.LE Q) : P = Q.induce ⋯

theorem Set.IndexedPartition.LE.eq {α : Type u_1} {s : Set α} {ι : Type u_2} {P Q : s.IndexedPartition ι} (hPQ : P.LE Q) : P = Q

@[simp]

theorem Set.IndexedPartition.le_refl {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) : P.LE P

theorem Set.IndexedPartition.induce_le {α : Type u_1} {s t : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (hts : t ⊆ s) : (P.induce hts).LE P

def Set.IndexedPartition.union {α : Type u_1} {s t : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (Q : t.IndexedPartition ι) (h : Disjoint s t) : (s ∪ t).IndexedPartition ι

Equations

• P.union Q h = { toFun := fun (i : ι) => P i ∪ Q i, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.union_apply {α : Type u_1} {s t : Set α} {ι : Type u_2} {i : ι} (P : s.IndexedPartition ι) (Q : t.IndexedPartition ι) {hdj : Disjoint s t} : (P.union Q hdj) i = P i ∪ Q i

def Set.IndexedPartition.single {α : Type u_1} {ι : Type u_2} [DecidableEq ι] (s : Set α) (i : ι) : s.IndexedPartition ι

The partition of s with part i equal to s and the other parts empty.

Equations

• Set.IndexedPartition.single s i = { toFun := fun (j : ι) => if j = i then s else ∅, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.single_apply {α : Type u_1} {ι : Type u_2} [DecidableEq ι] (s : Set α) (i : ι) : (IndexedPartition.single s i) i = s

theorem Set.IndexedPartition.single_apply_of_ne {α : Type u_1} {ι : Type u_2} {i j : ι} [DecidableEq ι] (s : Set α) (hne : j ≠ i) : (IndexedPartition.single s i) j = ∅

def Set.IndexedPartition.shift {α : Type u_1} {s : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) (t : Set α) (i : ι) : t.IndexedPartition ι

Turn a partition of s into a partition of t by intersecting each part with t, then adding the elements of t \ s into part i.

Equations

• P.shift t i = ((P.induce ⋯).union (Set.IndexedPartition.single (t \ s) i) ⋯).copy ⋯

@[simp]

theorem Set.IndexedPartition.shift_apply {α : Type u_1} {s : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) (t : Set α) (i : ι) : (P.shift t i) i = P i ∩ t ∪ t \ s

theorem Set.IndexedPartition.shift_apply_of_ne {α : Type u_1} {s : Set α} {ι : Type u_2} {i j : ι} [DecidableEq ι] (P : s.IndexedPartition ι) {t : Set α} (hne : j ≠ i) : (P.shift t i) j = P j ∩ t

theorem Set.IndexedPartition.shift_apply_eq_ite {α : Type u_1} {s : Set α} {ι : Type u_2} {j : ι} [DecidableEq ι] (P : s.IndexedPartition ι) (t : Set α) (i : ι) : (P.shift t i) j = if j = i then P j ∩ t ∪ t \ s else P j ∩ t

@[simp]

theorem Set.IndexedPartition.shift_copy {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) {t' : Set α} (h : t = t') (i : ι) : (P.shift t i).copy h = P.shift t' i

@[simp]

theorem Set.IndexedPartition.copy_shift {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) {s' : Set α} (h : s = s') (i : ι) : (P.copy h).shift t i = P.shift t i

def Set.IndexedPartition.expand {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) : s ⊆ t → (i : ι) → t.IndexedPartition ι

A version of shift where the new ground set is required to be a superset. Has better simp lemmas than shift.

Equations

• P.expand x✝ i = P.shift t i

theorem Set.IndexedPartition.expand_apply {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) (h : s ⊆ t) (i j : ι) : (P.expand h i) j = if j = i then P j ∪ t \ s else P j

@[simp]

theorem Set.IndexedPartition.expand_apply_self {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) (h : s ⊆ t) (i : ι) : (P.expand h i) i = P i ∪ t \ s

theorem Set.IndexedPartition.expand_apply_of_ne {α : Type u_1} {s t : Set α} {ι : Type u_2} {i j : ι} [DecidableEq ι] (P : s.IndexedPartition ι) (h : s ⊆ t) (hne : j ≠ i) : (P.expand h i) j = P j

@[simp]

theorem Set.IndexedPartition.expand_copy {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) {t' : Set α} (hst : s ⊆ t) (h : t = t') (i : ι) : (P.expand hst i).copy h = P.expand ⋯ i

@[simp]

theorem Set.IndexedPartition.copy_expand {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) {s' : Set α} (h : s = s') (hst : s' ⊆ t) (i : ι) : (P.copy h).expand hst i = P.expand ⋯ i

@[simp]

theorem Set.IndexedPartition.expand_induce {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) (h : s ⊆ t) (i : ι) : (P.expand h i).induce h = P

theorem Set.IndexedPartition.le_expand {α : Type u_1} {s t : Set α} {ι : Type u_2} [DecidableEq ι] (P : s.IndexedPartition ι) (h : s ⊆ t) (i : ι) : P.LE (P.expand h i)

def Set.IndexedPartition.diff {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (t : Set α) : (s \ t).IndexedPartition ι

Remove the elements of t from each cell of a partition of s to get a partition of s \ t.

Equations

• P.diff t = P.induce ⋯

@[simp]

theorem Set.IndexedPartition.diff_apply {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) (t : Set α) (i : ι) : (P.diff t) i = P i \ t

@[simp]

theorem Set.IndexedPartition.subset_of_diff {α : Type u_1} {s t : Set α} {ι : Type u_2} (P : (s \ t).IndexedPartition ι) (i : ι) : P i ⊆ s

@[simp]

theorem Set.IndexedPartition.disjoint_of_diff {α : Type u_1} {s t : Set α} {ι : Type u_2} (P : (s \ t).IndexedPartition ι) (i : ι) : Disjoint (P i) t

def Set.IndexedPartition.Trivial {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) : Prop

A partition is Trivial if it has at most one nonempty cell.

Equations

• P.Trivial = ∃ (i : ι), P i = s

theorem Set.IndexedPartition.trivial_def {α : Type u_1} {s : Set α} {ι : Type u_2} {P : s.IndexedPartition ι} : P.Trivial ↔ ∃ (i : ι), P i = s

theorem Set.IndexedPartition.Trivial.exists_eq_single {α : Type u_1} {s : Set α} {ι : Type u_2} {P : s.IndexedPartition ι} [DecidableEq ι] (h : P.Trivial) : ∃ (i : ι), P = IndexedPartition.single s i

theorem Set.IndexedPartition.trivial_of_subsingleton {α : Type u_1} {s : Set α} {ι : Type u_2} [Nonempty ι] (P : s.IndexedPartition ι) (h : s.Subsingleton) : P.Trivial

structure Set.IndexedPartition.Nontrivial {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) : Prop

A partition is nontrivial if all cells are nonempty. If there are at least three indices, this is not the negation of Partition.Trivial. Better name?

• nonempty (i : ι) : (P i).Nonempty

theorem Set.IndexedPartition.nontrivial_iff {α : Type u_1} {s : Set α} {ι : Type u_2} (P : s.IndexedPartition ι) : P.Nontrivial ↔ ∀ (i : ι), (P i).Nonempty

theorem Set.IndexedPartition.Nontrivial.ssubset {α : Type u_1} {s : Set α} {ι : Type u_2} {P : s.IndexedPartition ι} [Nontrivial ι] (h : P.Nontrivial) {i : ι} : P i ⊂ s

def Set.IndexedPartition.prod {α : Type u_1} {s : Set α} {ι η : Type} (P : s.IndexedPartition ι) (Q : s.IndexedPartition η) : s.IndexedPartition (ι × η)

Equations

• P.prod Q = { toFun := fun (i : ι × η) => P i.1 ∩ Q i.2, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.prod_apply {α : Type u_1} {s : Set α} {ι η : Type} (P : s.IndexedPartition ι) (Q : s.IndexedPartition η) (i : ι × η) : (P.prod Q) i = P i.1 ∩ Q i.2

def Set.IndexedPartition.comp {α : Type u_1} {s : Set α} {ι : Type u_2} {η : Type u_3} (P : s.IndexedPartition ι) (f : ι → η) : s.IndexedPartition η

Equations

• P.comp f = { toFun := fun (i : η) => ⋃ (j : ι), ⋃ (_ : f j = i), P j, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.comp_apply {α : Type u_1} {s : Set α} {ι : Type u_2} {η : Type u_3} (P : s.IndexedPartition ι) (f : ι → η) (i : η) : (P.comp f) i = ⋃ (j : ι), ⋃ (_ : f j = i), P j

theorem Set.IndexedPartition.comp_comp {α : Type u_1} {s : Set α} {ι : Type u_2} {η : Type u_4} {ξ : Type u_5} (P : s.IndexedPartition ι) (f : ι → η) (g : η → ξ) : (P.comp f).comp g = P.comp (g ∘ f)

theorem Set.IndexedPartition.comp_apply_equiv {α : Type u_1} {s : Set α} {ι : Type u_2} {η : Type u_3} (P : s.IndexedPartition ι) (f : ι ≃ η) (i : η) : (P.comp ⇑f) i = P (f.symm i)

theorem Set.IndexedPartition.ext_bool' {α : Type u_1} {s : Set α} {P P' : s.IndexedPartition Bool} (i : Bool) (h : P i = P' i) : P = P'

theorem Set.IndexedPartition.ext_bool {α : Type u_1} {s : Set α} {P P' : s.IndexedPartition Bool} (h : P true = P' true) : P = P'

theorem Set.IndexedPartition.ext_bool_iff {α : Type u_1} {s : Set α} {P P' : s.IndexedPartition Bool} (b : Bool) : P = P' ↔ P b = P' b

@[simp]

theorem Set.IndexedPartition.union_eq' {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : P false ∪ P true = s

@[simp]

theorem Set.IndexedPartition.union_eq {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : P true ∪ P false = s

@[simp]

theorem Set.IndexedPartition.union_bool_eq {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (b : Bool) : (P b ∪ P !b) = s

@[simp]

theorem Set.IndexedPartition.union_bool_eq' {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (b : Bool) : (P !b) ∪ P b = s

@[simp]

theorem Set.IndexedPartition.disjoint_true_false {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : Disjoint (P true) (P false)

@[simp]

theorem Set.IndexedPartition.disjoint_false_true {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : Disjoint (P false) (P true)

@[simp]

theorem Set.IndexedPartition.disjoint_bool {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (b : Bool) : Disjoint (P b) (P !b)

@[simp]

theorem Set.IndexedPartition.compl_eq {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (b : Bool) : s \ P b = P !b

theorem Set.IndexedPartition.compl_not_eq {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (b : Bool) : (s \ P !b) = P b

def Set.Disjoint.toIndexedPartition {α : Type u_1} {r s t : Set α} (disjoint : Disjoint r s) (union_eq : r ∪ s = t) : t.IndexedPartition Bool

Equations

• Set.Disjoint.toIndexedPartition disjoint union_eq = { toFun := fun (b : Bool) => bif b then r else s, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.Disjoint.toIndexedPartition_true {α : Type u_1} {r s t : Set α} {disjoint : Disjoint r s} {union_eq : r ∪ s = t} : (Disjoint.toIndexedPartition disjoint union_eq) true = r

@[simp]

theorem Set.Disjoint.toBipartition_false {α : Type u_1} {r s t : Set α} {disjoint : Disjoint r s} {union_eq : r ∪ s = t} : (Disjoint.toIndexedPartition disjoint union_eq) false = s

theorem Set.IndexedPartition.mem_or_mem {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) {a : α} (ha : a ∈ s) : a ∈ P true ∨ a ∈ P false

def Set.IndexedPartition.symm {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : s.IndexedPartition Bool

Equations

• P.symm = { toFun := fun (b : Bool) => P !b, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.symm_apply {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (b : Bool) : P.symm b = P !b

theorem Set.IndexedPartition.symm_true {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : P.symm true = P false

theorem Set.IndexedPartition.symm_false {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : P.symm false = P true

@[simp]

theorem Set.IndexedPartition.symm_symm {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : P.symm.symm = P

def Set.IndexedPartition.bSymm {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (b : Bool) : s.IndexedPartition Bool

If b is true, then P.symm, otherwise P.

Equations

• P.bSymm b = bif b then P.symm else P

@[simp]

theorem Set.IndexedPartition.bSymm_apply {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (b i : Bool) : (P.bSymm b) i = P (i != b)

@[simp]

theorem Set.IndexedPartition.bSymm_false {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : P.bSymm false = P

@[simp]

theorem Set.IndexedPartition.bSymm_true {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : P.bSymm true = P.symm

@[simp]

theorem Set.IndexedPartition.bSymm_bSymm {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (b c : Bool) : (P.bSymm b).bSymm c = P.bSymm (b != c)

theorem Set.IndexedPartition.compl_true {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : s \ P true = P false

@[simp]

theorem Set.IndexedPartition.compl_false {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : s \ P false = P true

theorem Set.IndexedPartition.trivial_of_eq {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} {i : Bool} (h : P i = s) : P.Trivial

theorem Set.IndexedPartition.trivial_of_eq_empty {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} {i : Bool} (h : P i = ∅) : P.Trivial

theorem Set.IndexedPartition.trivial_iff_eq_empty_or_eq_empty {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : P.Trivial ↔ P false = ∅ ∨ P true = ∅

theorem Set.IndexedPartition.trivial_iff_eq_or_eq {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : P.Trivial ↔ P false = s ∨ P true = s

theorem Set.IndexedPartition.trivial_def_bool {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (i : Bool) : P.Trivial ↔ P i = ∅ ∨ (P !i) = ∅

theorem Set.IndexedPartition.trivial_def_bool' {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (i : Bool) : P.Trivial ↔ P i = s ∨ (P !i) = s

theorem Set.IndexedPartition.Trivial.exists_eq {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (h : P.Trivial) : ∃ (b : Bool), P b = s

theorem Set.IndexedPartition.Trivial.exists_eq_empty {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (h : P.Trivial) : ∃ (b : Bool), P b = ∅

theorem Set.IndexedPartition.Trivial.exists_eq_eq {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (h : P.Trivial) : ∃ (b : Bool), P b = ∅ ∧ (P !b) = s

theorem Set.IndexedPartition.Trivial.symm {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (h : P.Trivial) : P.symm.Trivial

@[simp]

theorem Set.IndexedPartition.trivial_symm_iff {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : P.symm.Trivial ↔ P.Trivial

theorem Set.IndexedPartition.nontrivial_iff_and {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : P.Nontrivial ↔ (P false).Nonempty ∧ (P true).Nonempty

@[simp]

theorem Set.IndexedPartition.not_trivial_iff {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : ¬P.Trivial ↔ P.Nontrivial

@[simp]

theorem Set.IndexedPartition.not_nontrivial_iff {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : ¬P.Nontrivial ↔ P.Trivial

theorem Set.IndexedPartition.Nontrivial.not_trivial {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (h : P.Nontrivial) : ¬P.Trivial

theorem Set.IndexedPartition.Trivial.not_nontrivial {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (h : P.Trivial) : ¬P.Nontrivial

theorem Set.IndexedPartition.trivial_or_nontrivial {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) : P.Trivial ∨ P.Nontrivial

theorem Set.IndexedPartition.Nontrivial.symm {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} (h : P.Nontrivial) : P.symm.Nontrivial

@[simp]

theorem Set.IndexedPartition.nontrivial_symm_iff {α : Type u_1} {s : Set α} {P : s.IndexedPartition Bool} : P.symm.Nontrivial ↔ P.Nontrivial

@[simp]

theorem Set.IndexedPartition.induce_symm {α : Type u_1} {s t : Set α} (P : s.IndexedPartition Bool) (h : t ⊆ s) : (P.induce h).symm = P.symm.induce h

@[simp]

theorem Set.IndexedPartition.expand_apply_not {α : Type u_1} {s t : Set α} (P : s.IndexedPartition Bool) (h : s ⊆ t) (i : Bool) : ((P.expand h i) !i) = P !i

@[simp]

theorem Set.IndexedPartition.expand_not_apply {α : Type u_1} {s t : Set α} (P : s.IndexedPartition Bool) (h : s ⊆ t) (i : Bool) : (P.expand h !i) i = P i

@[simp]

theorem Set.IndexedPartition.expand_false_true {α : Type u_1} {s t : Set α} (P : s.IndexedPartition Bool) (h : s ⊆ t) : (P.expand h false) true = P true

@[simp]

theorem Set.IndexedPartition.expand_true_false {α : Type u_1} {s t : Set α} (P : s.IndexedPartition Bool) (h : s ⊆ t) : (P.expand h true) false = P false

@[simp]

theorem Set.IndexedPartition.expand_symm {α : Type u_1} {s t : Set α} (P : s.IndexedPartition Bool) (h : s ⊆ t) (i : Bool) : (P.expand h i).symm = P.symm.expand h !i

def Set.IndexedPartition.ofSubset {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (i : Bool) : t.IndexedPartition Bool

The bipartition of t with a subset s on side i, and t \ s on side !i.

Equations

• Set.IndexedPartition.ofSubset hst i = { toFun := fun (j : Bool) => bif j == i then s else t \ s, pairwise_disjoint' := ⋯, iUnion_eq' := ⋯ }

@[simp]

theorem Set.IndexedPartition.ofSubset_apply {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (i j : Bool) : (IndexedPartition.ofSubset hst i) j = bif j == i then s else t \ s

theorem Set.IndexedPartition.ofSubset_apply_self {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (i : Bool) : (IndexedPartition.ofSubset hst i) i = s

theorem Set.IndexedPartition.ofSubset_apply_not {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (i : Bool) : ((IndexedPartition.ofSubset hst i) !i) = t \ s

theorem Set.IndexedPartition.ofSubset_not_apply {α : Type u_1} {s t : Set α} (hst : s ⊆ t) (i : Bool) : (IndexedPartition.ofSubset hst !i) i = t \ s

theorem Set.IndexedPartition.ofSubset_true_false {α : Type u_1} {s t : Set α} (hst : s ⊆ t) : (IndexedPartition.ofSubset hst true) false = t \ s

theorem Set.IndexedPartition.ofSubset_false_true {α : Type u_1} {s t : Set α} (hst : s ⊆ t) : (IndexedPartition.ofSubset hst false) true = t \ s

@[simp]

theorem Set.IndexedPartition.ofSubset_copy {α : Type u_1} {r s t : Set α} {i : Bool} (hst : s ⊆ t) (htr : t = r) : (IndexedPartition.ofSubset hst i).copy htr = IndexedPartition.ofSubset ⋯ i

def Set.IndexedPartition.cross {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) (b c i : Bool) : s.IndexedPartition Bool

The bipartition whose i side is P b ∩ Q c and whose (!i) side is P !b ∪ Q !c. Varying b, c and i give the eight possible bipartitions arising from the 2x2 grid given by P and Q.

Equations

• P.cross Q b c i = (((P.bSymm b).prod (Q.bSymm c)).comp fun (p : Bool × Bool) => p.1 || p.2).bSymm i

@[simp]

theorem Set.IndexedPartition.cross_apply_self {α : Type u_1} {s : Set α} {i b c : Bool} (P Q : s.IndexedPartition Bool) : (P.cross Q b c i) i = P b ∩ Q c

@[simp]

theorem Set.IndexedPartition.cross_apply_not {α : Type u_1} {s : Set α} {i b c : Bool} (P Q : s.IndexedPartition Bool) : ((P.cross Q b c i) !i) = (P !b) ∪ Q !c

@[simp]

theorem Set.IndexedPartition.cross_not_apply {α : Type u_1} {s : Set α} {i b c : Bool} (P Q : s.IndexedPartition Bool) : (P.cross Q b c !i) i = (P !b) ∪ Q !c

theorem Set.IndexedPartition.cross_apply {α : Type u_1} {s : Set α} {i j b c : Bool} (P Q : s.IndexedPartition Bool) : (P.cross Q b c i) j = bif j == i then P b ∩ Q c else (P !b) ∪ Q !c

@[simp]

theorem Set.IndexedPartition.cross_symm {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) (b c i : Bool) : (P.cross Q b c i).symm = P.cross Q b c !i

@[simp]

theorem Set.IndexedPartition.cross_symm_left {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) (b c i : Bool) : P.symm.cross Q b c i = P.cross Q (!b) c i

@[simp]

theorem Set.IndexedPartition.cross_symm_right {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) (b c i : Bool) : P.cross Q.symm b c i = P.cross Q b (!c) i

@[simp]

theorem Set.IndexedPartition.cross_bSymm_left {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) (b b' c i : Bool) : (P.bSymm b').cross Q b c i = P.cross Q (b != b') c i

@[simp]

theorem Set.IndexedPartition.cross_bSymm_right {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) (b c c' i : Bool) : P.cross (Q.bSymm c') b c i = P.cross Q b (c != c') i

@[simp]

theorem Set.IndexedPartition.cross_bSymm {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) (b c i j : Bool) : (P.cross Q b c i).bSymm j = P.cross Q b c (i != j)

theorem Set.IndexedPartition.cross_comm {α : Type u_1} {s : Set α} {i : Bool} (P Q : s.IndexedPartition Bool) (b c : Bool) : P.cross Q b c i = Q.cross P c b i

theorem Set.IndexedPartition.Nontrivial.cross_trivial_iff {α : Type u_1} {s : Set α} {P Q : s.IndexedPartition Bool} (hP : P.Nontrivial) (b c i : Bool) : (P.cross Q b c i).Trivial ↔ P b ⊆ Q !c ∨ Q c ⊆ P !b

theorem Set.IndexedPartition.cross_trivial_iff {α : Type u_1} {s : Set α} {i : Bool} (P Q : s.IndexedPartition Bool) (b c : Bool) : (P.cross Q b c i).Trivial ↔ P b ⊆ Q !c ∨ Q c ⊆ P !b ∨ P b = s ∧ Q c = s

def Set.IndexedPartition.interCross {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : s.IndexedPartition Bool

The bipartition whose true side is P true ∩ Q true and whose false side is P false ∪ Q false

Equations

• P.interCross Q = P.cross Q true true true

def Set.IndexedPartition.unionCross {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : s.IndexedPartition Bool

The bipartition whose true side is P true ∪ Q true and whose false side is P false ∩ Q false

Equations

• P.unionCross Q = P.cross Q false false false

@[simp]

theorem Set.IndexedPartition.interCross_apply_true {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : (P.interCross Q) true = P true ∩ Q true

@[simp]

theorem Set.IndexedPartition.interCross_apply_false {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : (P.interCross Q) false = P false ∪ Q false

@[simp]

theorem Set.IndexedPartition.unionCross_apply_true {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : (P.unionCross Q) true = P true ∪ Q true

@[simp]

theorem Set.IndexedPartition.unionCross_apply_false {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : (P.unionCross Q) false = P false ∩ Q false

@[simp]

theorem Set.IndexedPartition.unionCross_symm {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : (P.unionCross Q).symm = P.symm.interCross Q.symm

@[simp]

theorem Set.IndexedPartition.interCross_symm {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : (P.interCross Q).symm = P.symm.unionCross Q.symm

theorem Set.IndexedPartition.interCross_comm {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : P.interCross Q = Q.interCross P

theorem Set.IndexedPartition.unionCross_comm {α : Type u_1} {s : Set α} (P Q : s.IndexedPartition Bool) : P.unionCross Q = Q.unionCross P

@[simp]

theorem Set.IndexedPartition.disjoint_inter_right {α : Type u_1} {r s t : Set α} (P : s.IndexedPartition Bool) : Disjoint (P true ∩ t) (P false ∩ r)

@[simp]

theorem Set.IndexedPartition.disjoint_inter_left {α : Type u_1} {r s t : Set α} (P : s.IndexedPartition Bool) : Disjoint (t ∩ P true) (r ∩ P false)

@[simp]

theorem Set.IndexedPartition.disjoint_bool_inter_right {α : Type u_1} {r s t : Set α} (P : s.IndexedPartition Bool) (i : Bool) : Disjoint (P i ∩ t) ((P !i) ∩ r)

@[simp]

theorem Set.IndexedPartition.disjoint_bool_inter_left {α : Type u_1} {r s t : Set α} (P : s.IndexedPartition Bool) (i : Bool) : Disjoint (t ∩ P i) (r ∩ P !i)

@[simp]

theorem Set.IndexedPartition.disjoint_bool_inter_right' {α : Type u_1} {r s t : Set α} (P : s.IndexedPartition Bool) (i : Bool) : Disjoint ((P !i) ∩ t) (P i ∩ r)

@[simp]

theorem Set.IndexedPartition.disjoint_bool_inter_left' {α : Type u_1} {r s t : Set α} (P : s.IndexedPartition Bool) (i : Bool) : Disjoint (t ∩ P !i) (r ∩ P i)

@[simp]

theorem Set.IndexedPartition.inter_ground_eq {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (b : Bool) : P b ∩ s = P b

theorem Set.IndexedPartition.union_inter_right' {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (X : Set α) (b : Bool) : P b ∩ X ∪ (P !b) ∩ X = X ∩ s

theorem Set.IndexedPartition.union_inter_left' {α : Type u_1} {s : Set α} (P : s.IndexedPartition Bool) (X : Set α) (b : Bool) : (X ∩ P b ∪ X ∩ P !b) = X ∩ s

theorem Set.IndexedPartition.union_inter_right {α : Type u_1} {s t : Set α} (P : s.IndexedPartition Bool) (h : t ⊆ s) (b : Bool) : P b ∩ t ∪ (P !b) ∩ t = t

theorem Set.IndexedPartition.union_inter_left {α : Type u_1} {s t : Set α} (P : s.IndexedPartition Bool) (h : t ⊆ s) (b : Bool) : (t ∩ P b ∪ t ∩ P !b) = t