Theorems · Theorem · order theory

liftFun_vecCons

∀ {α : Type u_1} {n : ℕ} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} {a : α},
  Relator.LiftFun (fun x1 x2 => x1 < x2) r (Matrix.vecCons a f) (Matrix.vecCons a f) ↔
    r a (f 0) ∧ Relator.LiftFun (fun x1 x2 => x1 < x2) r f f

Defined in

Mathlib.Order.Fin.Tuple

Cited by

4 results in Mathlib

Foundations

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

Assumes

IsTrans