Theorems · Theorem · order theory

List.not_of_mem_foldl_argAux

∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] {l : List α},
  Std.Irrefl r → IsTrans α r → ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ List.foldl (List.argAux r) o l → ¬r a m

Defined in

Mathlib.Data.List.MinMax

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableRel