inductive Which (α : Type) : Type

• wset {α : Type} : Finset α → Which α
• wbot {α : Type} : Which α

instance instZeroWhich {α : Type} : Zero (Which α)

Equations

• instZeroWhich = { zero := Which.wbot }

instance instAddWhich {α : Type} [DecidableEq α] : Add (Which α)

Equations

• One or more equations did not get rendered due to their size.

instance instMulWhich {α : Type} [DecidableEq α] : Mul (Which α)

Equations

• One or more equations did not get rendered due to their size.

instance instOneWhich {α : Type} : One (Which α)

Equations

• instOneWhich = { one := Which.wset ∅ }

instance instSubWhich {α : Type} [DecidableEq α] : Sub (Which α)

Equations

• One or more equations did not get rendered due to their size.

instance instLEWhich {α : Type} : LE (Which α)

Equations

• One or more equations did not get rendered due to their size.

instance instCommSemiringWhich {α : Type} [DecidableEq α] : CommSemiring (Which α)

Equations

• One or more equations did not get rendered due to their size.

instance instPartialOrderWhich {α : Type} : PartialOrder (Which α)

Equations

• instPartialOrderWhich = { toLE := instLEWhich, lt := fun (a b : Which α) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

instance instCanonicallyOrderedAddWhich {α : Type} [DecidableEq α] : CanonicallyOrderedAdd (Which α)

instance instIsOrderedAddMonoidWhich {α : Type} [DecidableEq α] : IsOrderedAddMonoid (Which α)

instance instSemiringWithMonusWhich {α : Type} [DecidableEq α] : SemiringWithMonus (Which α)

Equations

• One or more equations did not get rendered due to their size.

theorem Which.not_absorptive {α : Type} [DecidableEq α] (h : ∃ (x : α), ⊤) : ¬_root_.absorptive (Which α)

Which[X] is not absorptive as long as there is at least one variable

theorem Which.absorptive {α : Type} [DecidableEq α] (h : IsEmpty α) : _root_.absorptive (Which α)

Which[∅] is absorptive

theorem Which.idempotent {α : Type} [DecidableEq α] : _root_.idempotent (Which α)

theorem Which.not_mul_sub_left_distributive {α : Type} [DecidableEq α] [Inhabited α] : ¬mul_sub_left_distributive (Which α)

In Which[X], as long as X is non-empty, times is not distributive over monus.