Theorems · Theorem · combinatorics

Finset.Colex.erase_le_erase

∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a b : α} [inst_1 : DecidableEq α],
  a ∈ s → b ∈ s → (toColex (s.erase a) ≤ toColex (s.erase b) ↔ b ≤ a)

Defined in

Mathlib.Combinatorics.Colex

Cited by

2 results in Mathlib

Foundations

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

Assumes

PartialOrderDecidableEq