theorem sSupIndep.image {α : Type u_5} [CompleteLattice α] {S : Set α} (hS : sSupIndep S) {f : α → α} (hf : ∀ (i : α), f i ≤ i) : sSupIndep (f '' S)

theorem sSupIndep_subsingleton {α : Type u_5} [CompleteLattice α] {S : Set α} (hs : S.Subsingleton) : sSupIndep S

structure Partition (α : Type u_5) [CompleteLattice α] : Type u_5

• parts : Set α
• indep : sSupIndep self.parts
• bot_not_mem : ⊥ ∉ self.parts

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

Equations

• P.supp = sSup P.parts

@[instance_reducible]

instance Partition.instSetLike {α : Type u_1} [CompleteLattice α] : SetLike (Partition α) α

Equations

• Partition.instSetLike = { coe := Partition.parts, coe_injective := ⋯ }

@[simp]

theorem Partition.mem_parts {α : Type u_1} {x : α} [CompleteLattice α] {P : Partition α} : x ∈ P.parts ↔ x ∈ P

theorem Partition.coe_eq {α : Type u_1} [CompleteLattice α] (P : Partition α) : ↑P = P.parts

theorem Partition.ext_parts {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (hP : P.parts = Q.parts) : P = Q

theorem Partition.ext_iff_parts {α : Type u_1} [CompleteLattice α] {P Q : Partition α} : P = Q ↔ P.parts = Q.parts

theorem Partition.ext {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (hP : ∀ (x : α), x ∈ P ↔ x ∈ Q) : P = Q

theorem Partition.ext_iff {α : Type u_1} [CompleteLattice α] {P Q : Partition α} : P = Q ↔ ∀ (x : α), x ∈ P ↔ x ∈ Q

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

Equations

• P.subset Q = (P.parts ⊆ Q.parts)

instance Partition.instIsPartialOrderSubset {α : Type u_1} [CompleteLattice α] : IsPartialOrder (Partition α) fun (x1 x2 : Partition α) => x1.subset x2

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

Equations

• P.ssubset Q = (P.parts ⊂ Q.parts)

instance Partition.instIsStrictOrderSsubset {α : Type u_1} [CompleteLattice α] : IsStrictOrder (Partition α) fun (x1 x2 : Partition α) => x1.ssubset x2

instance Partition.instIsNonstrictStrictOrderSubsetSsubset {α : Type u_1} [CompleteLattice α] : IsNonstrictStrictOrder (Partition α) (fun (x1 x2 : Partition α) => x1.subset x2) fun (x1 x2 : Partition α) => x1.ssubset x2

theorem Partition.disjoint {α : Type u_1} {x y : α} [CompleteLattice α] {P : Partition α} (hx : x ∈ P) (hy : y ∈ P) (hxy : x ≠ y) : Disjoint x y

theorem Partition.eq_or_disjoint {α : Type u_1} {x y : α} [CompleteLattice α] {P : Partition α} (hx : x ∈ P) (hy : y ∈ P) : x = y ∨ Disjoint x y

theorem Partition.pairwiseDisjoint {α : Type u_1} [CompleteLattice α] {P : Partition α} : (↑P).PairwiseDisjoint id

theorem Partition.eq_of_not_disjoint {α : Type u_1} {x y : α} [CompleteLattice α] {P : Partition α} (hx : x ∈ P) (hy : y ∈ P) (hxy : ¬Disjoint x y) : x = y

theorem Partition.ne_bot_of_mem {α : Type u_1} {x : α} [CompleteLattice α] {P : Partition α} (hx : x ∈ P) : x ≠ ⊥

theorem Partition.bot_lt_of_mem {α : Type u_1} {x : α} [CompleteLattice α] {P : Partition α} (hx : x ∈ P) : ⊥ < x

theorem Partition.sSup_eq {α : Type u_1} [CompleteLattice α] (P : Partition α) : sSup ↑P = P.supp

theorem Partition.iSup_eq {α : Type u_1} [CompleteLattice α] (P : Partition α) : ⨆ x ∈ P, x = P.supp

theorem Partition.le_supp_of_mem {α : Type u_1} {x : α} [CompleteLattice α] {P : Partition α} (hx : x ∈ P) : x ≤ P.supp

theorem Partition.parts_nonempty {α : Type u_1} [CompleteLattice α] {P : Partition α} (hs : P.supp ≠ ⊥) : (↑P).Nonempty

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

theorem Partition.eq_of_subset_of_supp_eq {α : Type u_1} [CompleteLattice α] {P Q : Partition α} (hsu : P.subset Q) (hsupp : P.supp = Q.supp) : P = Q

theorem Partition.mem_of_subset_of_not_disjoint {α : Type u_1} {x : α} [CompleteLattice α] {P Q : Partition α} (hPQ : P.subset Q) (hxQ : x ∈ Q) (hndisj : ¬Disjoint P.supp x) : x ∈ P

theorem Partition.mem_iff_mem_of_parts_eq {α : Type u_1} {x : α} [CompleteLattice α] {P : Partition α} {S : Set α} (hP : P.parts = S) : x ∈ P ↔ x ∈ S

def Partition.ofPairwiseDisjoint {α : Type u_5} [Order.Frame α] {parts : Set α} (pairwiseDisjoint : parts.PairwiseDisjoint id) : Partition α

Equations

• Partition.ofPairwiseDisjoint pairwiseDisjoint = { parts := parts \ {⊥}, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.ofPairwiseDisjoint_parts {α : Type u_5} [Order.Frame α] {parts : Set α} (pairwiseDisjoint : parts.PairwiseDisjoint id) : (ofPairwiseDisjoint pairwiseDisjoint).parts = parts \ {⊥}

@[simp]

theorem Partition.mem_ofPairwiseDisjoint {α : Type u_5} [Order.Frame α] {x : α} {parts : Set α} (pairwiseDisjoint : parts.PairwiseDisjoint id) : x ∈ ofPairwiseDisjoint pairwiseDisjoint ↔ x ∈ parts \ {⊥}

@[simp]

theorem Partition.supp_ofPairwiseDisjoint {α : Type u_5} [Order.Frame α] {parts : Set α} (pairwiseDisjoint : parts.PairwiseDisjoint id) : (ofPairwiseDisjoint pairwiseDisjoint).supp = sSup parts

def Partition.ofPairwiseDisjoint' {α : Type u_5} [Order.Frame α] {parts : Set α} (pairwiseDisjoint : parts.PairwiseDisjoint id) (forall_nonempty : ∀ s ∈ parts, s ≠ ⊥) : Partition α

Equations

• Partition.ofPairwiseDisjoint' pairwiseDisjoint forall_nonempty = { parts := parts, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.ofPairwiseDisjoint'_parts {α : Type u_5} [Order.Frame α] {parts : Set α} (pairwiseDisjoint : parts.PairwiseDisjoint id) (forall_nonempty : ∀ s ∈ parts, s ≠ ⊥) : (ofPairwiseDisjoint' pairwiseDisjoint forall_nonempty).parts = parts

@[simp]

theorem Partition.supp_ofPairwiseDisjoint' {α : Type u_5} [Order.Frame α] {parts : Set α} (pairwiseDisjoint : parts.PairwiseDisjoint id) (forall_nonempty : ∀ s ∈ parts, s ≠ ⊥) : (ofPairwiseDisjoint' pairwiseDisjoint forall_nonempty).supp = sSup parts

@[simp]

theorem Partition.mem_ofPairwiseDisjoint' {α : Type u_5} [Order.Frame α] {x : α} {parts : Set α} (pairwiseDisjoint : parts.PairwiseDisjoint id) (forall_nonempty : ∀ s ∈ parts, s ≠ ⊥) : x ∈ ofPairwiseDisjoint' pairwiseDisjoint forall_nonempty ↔ x ∈ parts

theorem Partition.mem_of_mem_subset {α : Type u_5} [Order.Frame α] {x : α} {P Q : Partition α} (hPQ : P.subset Q) (hx : x ∈ Q) (hsupp : ¬Disjoint P.supp x) : x ∈ P

def Partition.ofIndependent {α : Type u_1} [CompleteLattice α] {u : Set α} (hs : sSupIndep u) (hbot : ⊥ ∉ u) : Partition α

A sSupIndep collection not containing ⊥ gives a partition of its supremum.

Equations

• Partition.ofIndependent hs hbot = { parts := u, indep := hs, bot_not_mem := hbot }

@[simp]

theorem Partition.ofIndependent_parts {α : Type u_1} [CompleteLattice α] {u : Set α} (hs : sSupIndep u) (hbot : ⊥ ∉ u) : (ofIndependent hs hbot).parts = u

@[simp]

theorem Partition.mem_ofIndependent_iff {α : Type u_1} [CompleteLattice α] {u : Set α} {a : α} (hu : sSupIndep u) (h : ⊥ ∉ u) : a ∈ ofIndependent hu h ↔ a ∈ u

@[simp]

theorem Partition.supp_ofIndependent {α : Type u_1} [CompleteLattice α] {u : Set α} (hu : sSupIndep u) (hbot : ⊥ ∉ u) : (ofIndependent hu hbot).supp = sSup u

def Partition.ofIndependent' {α : Type u_1} [CompleteLattice α] {u : Set α} (hs : sSupIndep u) : Partition α

A sSupIndep collection gives a partition of its supremum by removing ⊥.

Equations

• Partition.ofIndependent' hs = Partition.ofIndependent ⋯ ⋯

@[simp]

theorem Partition.ofIndependent'_parts {α : Type u_1} [CompleteLattice α] {u : Set α} (hs : sSupIndep u) : (ofIndependent' hs).parts = u \ {⊥}

@[simp]

theorem Partition.mem_ofIndependent'_iff {α : Type u_1} [CompleteLattice α] {u : Set α} {a : α} (hu : sSupIndep u) : a ∈ ofIndependent' hu ↔ a ∈ u ∧ a ≠ ⊥

@[simp]

theorem Partition.supp_ofIndependent' {α : Type u_1} [CompleteLattice α] {u : Set α} (hu : sSupIndep u) : (ofIndependent' hu).supp = sSup u

def Partition.empty (α : Type u_5) [CompleteLattice α] : Partition α

The partition with no parts.

Equations

• Partition.empty α = { parts := ∅, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.empty_parts (α : Type u_5) [CompleteLattice α] : (Partition.empty α).parts = ∅

@[instance_reducible]

instance Partition.instBot {α : Type u_1} [CompleteLattice α] : Bot (Partition α)

Equations

• Partition.instBot = { bot := Partition.empty α }

@[simp]

theorem Partition.parts_bot (α : Type u_5) [CompleteLattice α] : ⊥.parts = ∅

@[simp]

theorem Partition.notMem_bot {α : Type u_1} [CompleteLattice α] {a : α} : a ∉ ⊥

@[simp]

theorem Partition.parts_eq_empty_iff {α : Type u_1} [CompleteLattice α] (P : Partition α) : P.parts = ∅ ↔ P = ⊥

@[simp]

theorem Partition.supp_bot {α : Type u_1} [CompleteLattice α] : ⊥.supp = ⊥

@[simp]

theorem Partition.bot_coe_eq (α : Type u_5) [CompleteLattice α] : ↑⊥ = ∅

theorem Partition.eq_bot {α : Type u_1} [CompleteLattice α] {P : Partition α} (hP : P.supp = ⊥) : P = ⊥

@[simp]

theorem Partition.supp_eq_bot_iff {α : Type u_1} [CompleteLattice α] {P : Partition α} : P.supp = ⊥ ↔ P = ⊥

@[simp]

theorem Partition.bot_subset {α : Type u_1} [CompleteLattice α] (P : Partition α) : ⊥.subset P

@[simp]

theorem Partition.exists_mem_iff_ne_bot {α : Type u_1} [CompleteLattice α] (P : Partition α) : (∃ (x : α), x ∈ P) ↔ P ≠ ⊥

@[instance_reducible]

instance Partition.instUniqueOfSubsingleton {α : Type u_5} [CompleteLattice α] [Subsingleton α] : Unique (Partition α)

Equations

• Partition.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }

def Partition.indiscrete {α : Type u_1} [CompleteLattice α] (s : α) (hs : s ≠ ⊥) : Partition α

The one-part partition.

Equations

• Partition.indiscrete s hs = { parts := {s}, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.indiscrete_parts {α : Type u_1} [CompleteLattice α] (s : α) (hs : s ≠ ⊥) : (indiscrete s hs).parts = {s}

@[simp]

theorem Partition.mem_indiscrete_iff {α : Type u_1} {s : α} [CompleteLattice α] {a : α} (hs : s ≠ ⊥) : a ∈ indiscrete s hs ↔ a = s

@[simp]

theorem Partition.supp_indiscrete {α : Type u_1} {s : α} [CompleteLattice α] (hs : s ≠ ⊥) : (indiscrete s hs).supp = s

@[simp]

theorem Partition.indiscrete_subset_iff {α : Type u_1} {s : α} [CompleteLattice α] {P : Partition α} (hs : s ≠ ⊥) : (indiscrete s hs).subset P ↔ s ∈ P

theorem Partition.indiscrete_eq_iff {α : Type u_1} {s : α} [CompleteLattice α] {P : Partition α} (hs : s ≠ ⊥) : indiscrete s hs = P ↔ {s} = P.parts

def Partition.indiscrete' {α : Type u_1} [CompleteLattice α] (s : α) : Partition α

Similar to indiscrete, but in the case s = ⊥ it returns the empty partition.

Equations

• Partition.indiscrete' s = { parts := {T : α | s ≠ ⊥ ∧ T = s}, indep := ⋯, bot_not_mem := ⋯ }

@[simp]

theorem Partition.indiscrete'_parts {α : Type u_1} [CompleteLattice α] (s : α) : (indiscrete' s).parts = {T : α | s ≠ ⊥ ∧ T = s}

@[simp]

theorem Partition.mem_indiscrete'_iff {α : Type u_1} {s x : α} [CompleteLattice α] : x ∈ indiscrete' s ↔ s ≠ ⊥ ∧ x = s

@[simp]

theorem Partition.indiscrete'_eq_empty {α : Type u_1} [CompleteLattice α] : indiscrete' ⊥ = ⊥

@[simp]

theorem Partition.supp_indiscrete' {α : Type u_1} {s : α} [CompleteLattice α] : (indiscrete' s).supp = s

@[simp]

theorem Partition.indiscrete'_eq_of_ne_bot {α : Type u_1} {s : α} [CompleteLattice α] (hs : s ≠ ⊥) : indiscrete' s = indiscrete s hs

theorem Partition.eq_of_mem_indiscrete' {α : Type u_1} {s : α} [CompleteLattice α] {a : α} (has : a ∈ indiscrete' s) : a = s

theorem Partition.ne_bot_of_mem_indiscrete' {α : Type u_1} {s : α} [CompleteLattice α] {a : α} (has : a ∈ indiscrete' s) : a ≠ ⊥

def Partition.IsPartition {α : Type u_5} [CompleteLattice α] (S : Set α) : Prop

Equations

• Partition.IsPartition S = ∃ (P : Partition α), P.parts = S

@[simp]

theorem Partition.IsPartition.indep {α : Type u_5} [CompleteLattice α] {S : Set α} (hS : IsPartition S) : sSupIndep S

@[simp]

theorem Partition.IsPartition.bot_not_mem {α : Type u_5} [CompleteLattice α] {S : Set α} (hS : IsPartition S) : ⊥ ∉ S

theorem Partition.IsPartition.disjoint {α : Type u_5} [CompleteLattice α] {S : Set α} {x y : α} (hS : IsPartition S) (hx : x ∈ S) (hy : y ∈ S) (hxy : x ≠ y) : Disjoint x y

@[simp]

theorem Partition.IsPartition.eq_or_disjoint {α : Type u_5} [CompleteLattice α] {S : Set α} {x y : α} (hS : IsPartition S) (hx : x ∈ S) (hy : y ∈ S) : x = y ∨ Disjoint x y

@[simp]

theorem Partition.IsPartition.pairwiseDisjoint {α : Type u_5} [CompleteLattice α] {S : Set α} (hS : IsPartition S) : S.PairwiseDisjoint id

theorem Partition.IsPartition.eq_of_not_disjoint {α : Type u_5} [CompleteLattice α] {S : Set α} {x y : α} (hS : IsPartition S) (hx : x ∈ S) (hy : y ∈ S) (hxy : ¬Disjoint x y) : x = y

@[simp]

theorem Partition.IsPartition.ne_bot_of_mem {α : Type u_5} [CompleteLattice α] {S : Set α} {x : α} (hS : IsPartition S) (hx : x ∈ S) : x ≠ ⊥

theorem Partition.IsPartition.bot_lt_of_mem {α : Type u_5} [CompleteLattice α] {S : Set α} {x : α} (hS : IsPartition S) (hx : x ∈ S) : ⊥ < x

theorem Partition.IsPartition.iff_exists {α : Type u_5} [CompleteLattice α] {S : Set α} : IsPartition S ↔ ∃ (P : Partition α), P.parts = S

@[simp]

theorem Partition.exists_subset_iff_isPartition {α : Type u_5} [CompleteLattice α] {S : Set α} : (∃ (P : Partition α), S ⊆ P.parts) ↔ IsPartition S

theorem Partition.IsPartition.subset {α : Type u_5} [CompleteLattice α] {S T : Set α} (hS : IsPartition T) (hST : S ⊆ T) : IsPartition S

theorem Partition.parts_isPartition {α : Type u_5} [CompleteLattice α] (P : Partition α) : IsPartition P.parts

theorem Partition.isPartition_of_subset {α : Type u_5} [CompleteLattice α] {S : Set α} {P : Partition α} (hS : S ⊆ P.parts) : IsPartition S

theorem Partition.isPartition_of {α : Type u_5} [CompleteLattice α] {S : Set α} (h1 : sSupIndep S) (h2 : ⊥ ∉ S) : IsPartition S

theorem Partition.isPartition_iff {α : Type u_5} [CompleteLattice α] {S : Set α} : IsPartition S ↔ sSupIndep S ∧ ⊥ ∉ S

@[simp]

theorem Partition.isPartition_singleton_iff {α : Type u_5} [CompleteLattice α] {x : α} : IsPartition {x} ↔ x ≠ ⊥

theorem Partition.isPartition_pair_of_disjoint {α : Type u_5} [CompleteLattice α] {x y : α} (hx : x ≠ ⊥) (hy : y ≠ ⊥) (hxy : Disjoint x y) : IsPartition {x, y}

theorem Partition.isPartition_pair_of_mem {α : Type u_5} [CompleteLattice α] {x y : α} {P : Partition α} (hx : x ∈ P) (hy : y ∈ P) : IsPartition {x, y}

@[simp]

theorem Partition.isPartition_pair_iff {α : Type u_5} [CompleteLattice α] {x y : α} : IsPartition {x, y} ↔ (x = y ∨ Disjoint x y) ∧ x ≠ ⊥ ∧ y ≠ ⊥

theorem Partition.isPartition_iff_pairwiseDisjoint {α : Type u_1} {S : Set α} [Order.Frame α] : IsPartition S ↔ S.PairwiseDisjoint id ∧ ⊥ ∉ S

@[instance_reducible]

instance Partition.instPartialOrder {α : Type u_5} [CompleteLattice α] : PartialOrder (Partition α)

Equations

• Partition.instPartialOrder = { le := fun (P Q : Partition α) => ∀ x ∈ P, ∃ y ∈ Q, x ≤ y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Partition.le_def {α : Type u_5} [CompleteLattice α] {P Q : Partition α} : P ≤ Q ↔ ∀ x ∈ P, ∃ y ∈ Q, x ≤ y

theorem Partition.exists_le_of_mem_le {α : Type u_5} [CompleteLattice α] {x : α} {P Q : Partition α} (h : P ≤ Q) (hx : x ∈ P) : ∃ y ∈ Q, x ≤ y

theorem Partition.exists_unique_of_mem_le {α : Type u_5} [CompleteLattice α] {x : α} {P Q : Partition α} (h : P ≤ Q) (hx : x ∈ P) : ∃! y : α, y ∈ Q ∧ x ≤ y

theorem Partition.le_of_supp_le_part {α : Type u_5} [CompleteLattice α] {P Q : Partition α} {a : α} (ha : a ∈ P) (hQa : Q.supp ≤ a) : Q ≤ P

@[instance_reducible]

instance Partition.instOrderTop {α : Type u_5} [CompleteLattice α] : OrderTop (Partition α)

Equations

• Partition.instOrderTop = { top := Partition.ofIndependent' ⋯, le_top := ⋯ }

@[simp]

theorem Partition.supp_top {α : Type u_5} [CompleteLattice α] : ⊤.supp = ⊤

@[simp]

theorem Partition.parts_top {α : Type u_5} [CompleteLattice α] [Nontrivial α] : ⊤.parts = {⊤}

@[simp]

theorem Partition.top_parts {α : Type u_5} [CompleteLattice α] (hs : ⊤ ≠ ⊥) : ↑⊤ = {⊤}

@[simp]

theorem Partition.mem_top_iff {α : Type u_5} [CompleteLattice α] {a : α} : a ∈ ⊤ ↔ a = ⊤ ∧ a ≠ ⊥

theorem Partition.top_eq_indiscrete {α : Type u_5} [CompleteLattice α] (hs : ⊤ ≠ ⊥) : ⊤ = indiscrete ⊤ hs

theorem Partition.parts_top_subset {α : Type u_5} [CompleteLattice α] : ↑⊤ ⊆ {⊤}

@[instance_reducible]

instance Partition.instOrderBot {α : Type u_5} [CompleteLattice α] : OrderBot (Partition α)

Equations

• Partition.instOrderBot = { toBot := Partition.instBot, bot_le := ⋯ }

@[simp]

theorem Partition.bot_parts {α : Type u_5} [CompleteLattice α] : ⊥.parts = ∅

@[simp]

theorem Partition.bot_supp {α : Type u_5} [CompleteLattice α] : ⊥.supp = ⊥

theorem Partition.supp_le_of_le {α : Type u_5} [CompleteLattice α] {P Q : Partition α} (h : P ≤ Q) : P.supp ≤ Q.supp

theorem Partition.le_of_subset {α : Type u_5} [CompleteLattice α] {P Q : Partition α} (h : P.subset Q) : P ≤ Q

instance Partition.instNontrivial {α : Type u_5} [CompleteLattice α] [Nontrivial α] : Nontrivial (Partition α)

def Partition.Atomic {α : Type u_5} [CompleteLattice α] (P : Partition α) : Prop

Equations

• P.Atomic = ∀ x ∈ P, IsAtom x

theorem Partition.Atomic.subset_iff_le {α : Type u_5} [CompleteLattice α] {P Q : Partition α} (hQ : Q.Atomic) : P.subset Q ↔ P ≤ Q

theorem Partition.Atomic.atomic_of_subset {α : Type u_5} [CompleteLattice α] {P Q : Partition α} (hPQ : P.subset Q) (hQ : Q.Atomic) : P.Atomic

theorem Partition.Atomic.atomic_of_le {α : Type u_5} [CompleteLattice α] {P Q : Partition α} (hPQ : P ≤ Q) (hQ : Q.Atomic) : P.Atomic

@[simp]

theorem Partition.bot_atomic {α : Type u_5} [CompleteLattice α] : ⊥.Atomic

theorem Partition.exists_atomic {α : Type u_5} [CompleteLattice α] (s : α) [IsAtomistic α] [IsModularLattice α] [IsCompactlyGenerated α] : ∃ (P : Partition α), P.Atomic ∧ P.supp = s