Theorems · Definition · order theory

Finset.SupIndep

{α : Type u_1} → {ι : Type u_3} → [inst : Lattice α] → [OrderBot α] → Finset ι → (ι → α) → Prop

Supremum independence of finite sets. We avoid the "obvious" definition using s.erase i because erase would require decidable equality on ι.

Defined in

Mathlib.Order.SupIndep

Cited by

52 results in Mathlib

Foundations

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

Assumes

LatticeOrderBot