def Partition.induce {α : Type u_1} [CompleteLattice α] (P : Partition α) (a : α) : Partition α

Equations

• P.induce a = Partition.ofIndependent' ⋯

@[simp]

theorem Partition.induce_parts {α : Type u_1} [CompleteLattice α] (P : Partition α) (a : α) : (P.induce a).parts = (fun (x : α) => a ⊓ x) '' P.parts \ {⊥}

@[simp]

theorem Partition.induce_supp {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : (P.induce a).supp = ⨆ t ∈ P, a ⊓ t

@[simp]

theorem Partition.mem_induce_iff {α : Type u_1} {a x : α} [CompleteLattice α] {P : Partition α} : x ∈ P.induce a ↔ x ≠ ⊥ ∧ ∃ t ∈ P, a ⊓ t = x

theorem Partition.inf_mem_induce {α : Type u_1} {a x : α} [CompleteLattice α] {P : Partition α} (h : x ∈ P) (hne : a ⊓ x ≠ ⊥) : a ⊓ x ∈ P.induce a

@[simp]

theorem Partition.induce_empty {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.induce ⊥ = ⊥

@[simp]

theorem Partition.induce_induce {α : Type u_1} {a b : α} [CompleteLattice α] {P : Partition α} : (P.induce a).induce b = P.induce (b ⊓ a)

@[simp]

theorem Partition.induce_eq_self_iff {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : P.induce a = P ↔ P.supp ≤ a

@[simp]

theorem Partition.induce_self {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.induce P.supp = P

@[simp]

theorem Partition.induce_le {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : P.induce a ≤ P

theorem Partition.induce_le_induce_right {α : Type u_1} {a b : α} [CompleteLattice α] {P : Partition α} (h : a ⊓ P.supp ≤ b ⊓ P.supp) : P.induce a ≤ P.induce b

theorem Partition.induce_le_induce_right_of_le {α : Type u_1} {a b : α} [CompleteLattice α] {P : Partition α} (h : a ≤ b) : P.induce a ≤ P.induce b

theorem Partition.induce_le_induce_left {α : Type u_1} {a : α} [CompleteLattice α] {P Q : Partition α} (hPQ : P ≤ Q) : P.induce a ≤ Q.induce a

theorem Partition.le_induce_of_supp_le {α : Type u_1} {a : α} [CompleteLattice α] {P Q : Partition α} (hPQ : P ≤ Q) (hP : P.supp ≤ a) : P ≤ Q.induce a

theorem Partition.induce_subset_induce_of_subset {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (hPQ : P.subset Q) (a : α) : (P.induce a).subset (Q.induce a)

theorem Partition.subset_induce_of_supp_le {α : Type u_1} {a : α} [CompleteLattice α] {P Q : Partition α} (hPQ : P.subset Q) (hP : P.supp ≤ a) : P.subset (Q.induce a)

theorem Partition.induce_eq_induce_right {α : Type u_1} {a b : α} [CompleteLattice α] {P : Partition α} (h : a ⊓ P.supp = b ⊓ P.supp) : P.induce a = P.induce b

def Partition.isInducedSubpartition {α : Type u_1} [CompleteLattice α] (P Q : Partition α) : Prop

Equations

• P.isInducedSubpartition Q = (Q.induce P.supp = P)

def Partition.«term_≤ip_» : Lean.TrailingParserDescr

Equations

• Partition.«term_≤ip_» = Lean.ParserDescr.trailingNode `Partition.«term_≤ip_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ip ") (Lean.ParserDescr.cat `term 51))

theorem Partition.isInducedSubpartition_iff {α : Type u_1} [CompleteLattice α] {P Q : Partition α} : P.isInducedSubpartition Q ↔ Q.induce P.supp = P

theorem Partition.isInducedSubpartition.le {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (h : P.isInducedSubpartition Q) : P ≤ Q

theorem Partition.isInducedSubpartition.supp_le {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (h : P.isInducedSubpartition Q) : P.supp ≤ Q.supp

theorem Partition.isInducedSubpartition_of_subset {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (hPQ : P.subset Q) : P.isInducedSubpartition Q

theorem Partition.isInducedSubpartition.eq_of_supp_le {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (hPQ : P.isInducedSubpartition Q) (hQP : Q.supp ≤ P.supp) : P = Q

@[simp]

theorem Partition.isInducedSubpartition_rfl {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.isInducedSubpartition P

instance Partition.instReflIsInducedSubpartition {α : Type u_1} [CompleteLattice α] : Std.Refl isInducedSubpartition

theorem Partition.isInducedSubpartition.antisymm {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (hPQ : P.isInducedSubpartition Q) (hQP : Q.isInducedSubpartition P) : P = Q

instance Partition.instAntisymmIsInducedSubpartition {α : Type u_1} [CompleteLattice α] : Std.Antisymm isInducedSubpartition

@[simp]

theorem Partition.induce_supp' {α : Type u_1} [Order.Frame α] (P : Partition α) (a : α) : (P.induce a).supp = a ⊓ P.supp

theorem Partition.induce_le_induce_iff {α : Type u_1} [Order.Frame α] {P : Partition α} {a b : α} : P.induce a ≤ P.induce b ↔ a ⊓ P.supp ≤ b ⊓ P.supp

theorem Partition.induce_eq_induce_iff {α : Type u_1} [Order.Frame α] {P : Partition α} {a b : α} : P.induce a = P.induce b ↔ a ⊓ P.supp = b ⊓ P.supp

theorem Partition.inter_mem_induce {α : Type u_1} [Order.Frame α] {P : Partition α} {a b : α} (hne : ¬Disjoint a b) (ht : b ∈ P) : a ⊓ b ∈ P.induce a

theorem Partition.isInducedSubpartition.trans {α : Type u_1} [Order.Frame α] {P Q R : Partition α} (hPQ : P.isInducedSubpartition Q) (hQR : Q.isInducedSubpartition R) : P.isInducedSubpartition R

theorem Partition.isInducedSubpartition.of_supp_le {α : Type u_1} [Order.Frame α] {P Q R : Partition α} (hPQ : P.supp ≤ Q.supp) (hPR : P.isInducedSubpartition R) (hQR : Q.isInducedSubpartition R) : P.isInducedSubpartition Q

def Partition.delete {α : Type u_1} [CompleteLattice α] (P : Partition α) (s : Set α) : Partition α

P \ s is the subpartition of P with parts P.parts \ s.

Equations

• P.delete s = { parts := P.parts \ s, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.delete_parts {α : Type u_1} [CompleteLattice α] (P : Partition α) (s : Set α) : (P.delete s).parts = P.parts \ s

def Partition.«term_\_» : Lean.TrailingParserDescr

Equations

• Partition.«term_\_» = Lean.ParserDescr.trailingNode `Partition.«term_\_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem Partition.mem_delete_iff {α : Type u_1} {s : Set α} {x : α} [CompleteLattice α] {P : Partition α} : x ∈ P.delete s ↔ x ∈ P ∧ x ∉ s

@[simp]

theorem Partition.delete_supp {α : Type u_1} {s : Set α} [CompleteLattice α] {P : Partition α} : (P.delete s).supp = sSup (P.parts \ s)

theorem Partition.delete_subset {α : Type u_1} [CompleteLattice α] {P : Partition α} (s : Set α) : (P.delete s).subset P

theorem Partition.delete_le {α : Type u_1} [CompleteLattice α] {P : Partition α} (s : Set α) : P.delete s ≤ P

@[simp]

theorem Partition.delete_empty {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.delete ∅ = P

@[simp]

theorem Partition.delete_univ {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.delete Set.univ = ⊥

@[simp]

theorem Partition.delete_self {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.delete P.parts = ⊥

@[simp]

theorem Partition.delete_delete {α : Type u_1} {s t : Set α} [CompleteLattice α] {P : Partition α} : (P.delete s).delete t = P.delete (s ∪ t)

theorem Partition.delete_subset_delete_of_subset {α : Type u_1} {s t : Set α} [CompleteLattice α] {P : Partition α} (h : s ⊆ t) : (P.delete t).subset (P.delete s)

theorem Partition.delete_le_delete_of_subset {α : Type u_1} {s t : Set α} [CompleteLattice α] {P : Partition α} (h : s ⊆ t) : P.delete t ≤ P.delete s

theorem Partition.delete_subset_of_subset {α : Type u_1} {s : Set α} [CompleteLattice α] {P Q : Partition α} (hPQ : P.subset Q) : (P.delete s).subset (Q.delete s)

theorem Partition.delete_supp_le {α : Type u_1} {s : Set α} [CompleteLattice α] {P : Partition α} : (P.delete s).supp ≤ P.supp

def Partition.restrict {α : Type u_1} [CompleteLattice α] (P : Partition α) (s : Set α) (hs : s ⊆ P.parts) : Partition α

The subpartition with over a subset of the parts.

Equations

• P.restrict s hs = { parts := s, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.restrict_parts {α : Type u_1} [CompleteLattice α] (P : Partition α) (s : Set α) (hs : s ⊆ P.parts) : (P.restrict s hs).parts = s

@[simp]

theorem Partition.mem_restrict_iff {α : Type u_1} {s : Set α} {a : α} [CompleteLattice α] {P : Partition α} (hs : s ⊆ P.parts) : a ∈ P.restrict s hs ↔ a ∈ s

@[simp]

theorem Partition.restrict_supp {α : Type u_1} {s : Set α} [CompleteLattice α] {P : Partition α} (hs : s ⊆ P.parts) : (P.restrict s hs).supp = sSup s

theorem Partition.restrict_subset {α : Type u_1} {s : Set α} [CompleteLattice α] {P : Partition α} (hs : s ⊆ P.parts) : (P.restrict s hs).subset P

theorem Partition.restrict_le {α : Type u_1} {s : Set α} [CompleteLattice α] {P : Partition α} (hs : s ⊆ P.parts) : P.restrict s hs ≤ P

theorem Partition.subset_iff_restrict {α : Type u_1} [CompleteLattice α] {P Q : Partition α} : P.subset Q ↔ ∃ (S : Set α) (hS : S ⊆ Q.parts), Q.restrict S hS = P

@[simp]

theorem Partition.restrict_eq_self_iff {α : Type u_1} {s : Set α} [CompleteLattice α] {P : Partition α} (hs : s ⊆ P.parts) : P.restrict s hs = P ↔ s = P.parts

def Partition.cover {α : Type u_1} [CompleteLattice α] (P : Partition α) (a : α) : Partition α

Equations

• P.cover a = P.restrict {s : α | s ∈ P.parts ∧ ¬Disjoint a s} ⋯

@[simp]

theorem Partition.cover_parts {α : Type u_1} [CompleteLattice α] (P : Partition α) (a : α) : (P.cover a).parts = {s : α | s ∈ P ∧ ¬Disjoint a s}

@[simp]

theorem Partition.mem_cover_iff {α : Type u_1} {a x : α} [CompleteLattice α] {P : Partition α} : x ∈ P.cover a ↔ x ∈ P ∧ ¬Disjoint a x

@[simp]

theorem Partition.cover_supp {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : (P.cover a).supp = sSup {s : α | s ∈ P.parts ∧ ¬Disjoint a s}

theorem Partition.cover_supp_le {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : (P.cover a).supp ≤ P.supp

theorem Partition.cover_supp_eq_self {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.cover P.supp = P

theorem Partition.cover_subset {α : Type u_1} [CompleteLattice α] {P : Partition α} (a : α) : (P.cover a).subset P

theorem Partition.cover_le_of_le {α : Type u_1} {a : α} [CompleteLattice α] {P Q : Partition α} (h : Q ≤ P) : Q.cover a ≤ P.cover a

@[simp]

theorem Partition.cover_eq_self_iff {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : P.cover a = P ↔ ∀ x ∈ P, ¬Disjoint a x

theorem Partition.induce_le_cover {α : Type u_1} [CompleteLattice α] (P : Partition α) (a : α) : P.induce a ≤ P.cover a

def Partition.avoid {α : Type u_1} [CompleteLattice α] (P : Partition α) (a : α) : Partition α

Equations

• P.avoid a = P.restrict {s : α | s ∈ P.parts ∧ Disjoint a s} ⋯

@[simp]

theorem Partition.mem_avoid_iff {α : Type u_1} {a x : α} [CompleteLattice α] {P : Partition α} : x ∈ P.avoid a ↔ x ∈ P ∧ Disjoint a x

@[simp]

theorem Partition.avoid_supp {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : (P.avoid a).supp = sSup {s : α | s ∈ P.parts ∧ Disjoint a s}

theorem Partition.avoid_supp_le {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : (P.avoid a).supp ≤ P.supp

theorem Partition.avoid_supp_eq_self {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.avoid ⊥ = P

theorem Partition.avoid_subset {α : Type u_1} [CompleteLattice α] {P : Partition α} (a : α) : (P.avoid a).subset P

@[simp]

theorem Partition.avoid_eq_self_iff {α : Type u_1} {a : α} [CompleteLattice α] {P : Partition α} : P.avoid a = P ↔ ∀ x ∈ P, Disjoint a x

def Partition.Agree {α : Type u_1} [CompleteLattice α] (P Q : Partition α) : Prop

Equations

• P.Agree Q = ∃ (S : Partition α), P.subset S ∧ Q.subset S

theorem Partition.agree_of_subset_subset {α : Type u_1} [CompleteLattice α] {P P₀ Q₀ : Partition α} (hP : P₀.subset P) (hQ : Q₀.subset P) : P₀.Agree Q₀

@[simp]

theorem Partition.Agree.rfl {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.Agree P

instance Partition.instReflAgree {α : Type u_1} [CompleteLattice α] : Std.Refl Agree

theorem Partition.Agree.symm {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (h : P.Agree Q) : Q.Agree P

instance Partition.instSymmAgree {α : Type u_1} [CompleteLattice α] : Std.Symm Agree

theorem Partition.agree_comm {α : Type u_1} [CompleteLattice α] {P Q : Partition α} : P.Agree Q ↔ Q.Agree P

@[simp]

theorem Partition.Agree.mem_of_mem {α : Type u_1} {a : α} [CompleteLattice α] {P Q : Partition α} (h : P.Agree Q) (hx : a ∈ P) (hndisj : ¬Disjoint Q.supp a) : a ∈ Q

theorem Partition.Agree.eq_of_not_disjoint {α : Type u_1} {a b : α} [CompleteLattice α] {P Q : Partition α} (h : P.Agree Q) (ha : a ∈ P) (hb : b ∈ Q) (hndisj : ¬Disjoint a b) : a = b

theorem Partition.Agree.mem_or_disjoint {α : Type u_1} {a : α} [CompleteLattice α] {P Q : Partition α} (h : P.Agree Q) (ha : a ∈ P) : a ∈ Q ∨ Disjoint Q.supp a

theorem Partition.Agree.mono_left {α : Type u_1} [CompleteLattice α] {P Q P₀ : Partition α} (h : P.Agree Q) (hP : P₀.subset P) : P₀.Agree Q

theorem Partition.Agree.mono_right {α : Type u_1} [CompleteLattice α] {P Q Q₀ : Partition α} (h : P.Agree Q) (hQ : Q₀.subset Q) : P.Agree Q₀

theorem Partition.Agree.mono {α : Type u_1} [CompleteLattice α] {P Q P₀ Q₀ : Partition α} (h : P.Agree Q) (hP : P₀.subset P) (hQ : Q₀.subset Q) : P₀.Agree Q₀

@[simp]

theorem Partition.indiscrete_agree_indiscrete_iff {α : Type u_1} {a b : α} [CompleteLattice α] (ha : a ≠ ⊥) (hb : b ≠ ⊥) : (indiscrete a ha).Agree (indiscrete b hb) ↔ a = b ∨ Disjoint a b

@[simp]

theorem Partition.agree_on_indiscrete'_iff {α : Type u_1} {a b : α} [CompleteLattice α] : Function.onFun Agree indiscrete' a b ↔ a = b ∨ Disjoint a b

@[simp]

theorem Partition.cover_eq_bot_iff {α : Type u_1} {a : α} [Order.Frame α] {P : Partition α} : P.cover a = ⊥ ↔ ∀ x ∈ P, Disjoint a x

theorem Partition.induce_sSup_eq_restrict {α : Type u_1} [Order.Frame α] (P : Partition α) (a : α) : P.induce (sSup {s : α | s ∈ P.parts ∧ ¬Disjoint a s}) = P.restrict {s : α | s ∈ P.parts ∧ ¬Disjoint a s} ⋯

theorem Partition.agree_iff_union_pairwiseDisjoint {α : Type u_1} [Order.Frame α] {P Q : Partition α} : P.Agree Q ↔ (P.parts ∪ Q.parts).PairwiseDisjoint id

theorem Partition.sSupIndep_parts_union_of_mem_of_not_disjoint {α : Type u_1} [Order.Frame α] {P Q : Partition α} (h : ∀ x ∈ P, ¬Disjoint Q.supp x → x ∈ Q) : sSupIndep (P.parts ∪ Q.parts)

theorem Partition.agree_of_mem_of_not_disjoint {α : Type u_1} [Order.Frame α] {P Q : Partition α} (h : ∀ x ∈ P, ¬Disjoint Q.supp x → x ∈ Q) : P.Agree Q

theorem Partition.agree_iff_mem_of_not_disjoint {α : Type u_1} [Order.Frame α] {P Q : Partition α} : P.Agree Q ↔ ∀ x ∈ P, ¬Disjoint Q.supp x → x ∈ Q

theorem Partition.agree_of_supp_disjoint {α : Type u_1} [Order.Frame α] {P Q : Partition α} (h : Disjoint P.supp Q.supp) : P.Agree Q

theorem Partition.set_pairwise_agree_iff_sUnion_pairwiseDisjoint {α : Type u_1} [Order.Frame α] {Ps : Set (Partition α)} : Ps.Pairwise Agree ↔ (⋃ P ∈ Ps, P.parts).PairwiseDisjoint id

def Partition.ofSetPairwiseAgree {α : Type u_1} [Order.Frame α] (Ps : Set (Partition α)) (h : Ps.Pairwise Agree) : Partition α

Equations

• Partition.ofSetPairwiseAgree Ps h = Partition.ofPairwiseDisjoint ⋯

@[simp]

theorem Partition.ofSetPairwiseAgree_parts {α : Type u_1} [Order.Frame α] {Ps : Set (Partition α)} (h : Ps.Pairwise Agree) : (ofSetPairwiseAgree Ps h).parts = ⋃ P ∈ Ps, P.parts

@[simp]

theorem Partition.ofSetPairwiseAgree_supp {α : Type u_1} [Order.Frame α] {Ps : Set (Partition α)} (h : Ps.Pairwise Agree) : (ofSetPairwiseAgree Ps h).supp = ⨆ P ∈ Ps, P.supp

theorem Partition.ofSetPairwiseAgree_subset_of_mem {α : Type u_1} [Order.Frame α] {P : Partition α} {Ps : Set (Partition α)} (h : Ps.Pairwise Agree) (hP : P ∈ Ps) : P.subset (ofSetPairwiseAgree Ps h)