Theorems · Definition · order theory

Finset.disjSups

{α : Type u_2} →
  [DecidableEq α] →
    [inst : SemilatticeSup α] → [inst_1 : OrderBot α] → [DecidableRel Disjoint] → Finset α → Finset α → Finset α

The finset of elements of the form a ⊔ b where a ∈ s, b ∈ t and a and b are disjoint.

Defined in

Mathlib.Data.Finset.Sups

Cited by

22 results in Mathlib

Foundations

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

Assumes

DecidableEqSemilatticeSupOrderBotDecidableRel