Theorems · Theorem · order theory

Partition.mem_removeBot

∀ {α : Type u_1} {s x : α} [inst : CompleteLattice α] (P : Set α) (indep : sSupIndep P) (hsSup : sSup P = s),
  x ∈ Partition.removeBot P indep hsSup ↔ x ∈ P ∧ x ≠ ⊥

Defined in

Mathlib.Order.Partition.Basic

Cited by

1 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLattice