Documentation

Lean.Elab.Tactic.Omega.MinNatAbs

List.nonzeroMinimum, List.minNatAbs, List.maxNatAbs #

List.minNatAbs computes the minimum non-zero absolute value of a List Int. This is not generally useful outside of the implementation of the omega tactic, so we keep it in the Lean/Elab/Tactic/Omega directory (although the definitions are in the List namespace).

The minimum non-zero entry in a list of natural numbers, or zero if all entries are zero.

We completely characterize the function via nonzeroMinimum_eq_zero_iff and nonzeroMinimum_eq_nonzero_iff below.

Equations
Instances For
    theorem List.min?_eq_some_iff'' {a : Nat} {xs : List Nat} :
    xs.min? = some a a xs ∀ (b : Nat), b xsa b
    @[simp]
    theorem List.nonzeroMinimum_eq_zero_iff {xs : List Nat} :
    xs.nonzeroMinimum = 0 ∀ (x : Nat), x xsx = 0
    theorem List.nonzeroMinimum_mem {xs : List Nat} (w : xs.nonzeroMinimum 0) :
    xs.nonzeroMinimum xs
    theorem List.nonzeroMinimum_pos {a : Nat} {xs : List Nat} (m : a xs) (h : a 0) :
    0 < xs.nonzeroMinimum
    theorem List.nonzeroMinimum_le {a : Nat} {xs : List Nat} (m : a xs) (h : a 0) :
    xs.nonzeroMinimum a
    theorem List.nonzeroMinimum_eq_nonzero_iff {xs : List Nat} {y : Nat} (h : y 0) :
    xs.nonzeroMinimum = y y xs ∀ (x : Nat), x xsy x x = 0
    theorem List.nonzeroMinimum_eq_of_nonzero {xs : List Nat} (h : xs.nonzeroMinimum 0) :
    ∃ (x : Nat), x xs xs.nonzeroMinimum = x
    theorem List.nonzeroMinimum_le_iff {xs : List Nat} {y : Nat} :
    xs.nonzeroMinimum y xs.nonzeroMinimum = 0 ∃ (x : Nat), x xs x y x 0
    theorem List.nonzeroMininum_map_le_nonzeroMinimum {α : Type u_1} {β : Type u_2} (f : αβ) (p : αNat) (q : βNat) (xs : List α) (h : ∀ (a : α), a xs(p a = 0 q (f a) = 0)) (w : ∀ (a : α), a xsp a 0q (f a) p a) :
    (List.map q (List.map f xs)).nonzeroMinimum (List.map p xs).nonzeroMinimum

    The minimum absolute value of a nonzero entry, or zero if all entries are zero.

    We completely characterize the function via minNatAbs_eq_zero_iff and minNatAbs_eq_nonzero_iff below.

    Equations
    Instances For
      @[simp]
      theorem List.minNatAbs_eq_zero_iff {xs : List Int} :
      xs.minNatAbs = 0 ∀ (y : Int), y xsy = 0
      theorem List.minNatAbs_eq_nonzero_iff {z : Nat} (xs : List Int) (w : z 0) :
      xs.minNatAbs = z (∃ (y : Int), y xs y.natAbs = z) ∀ (y : Int), y xsz y.natAbs y = 0
      @[simp]
      theorem List.minNatAbs_nil :
      [].minNatAbs = 0

      The maximum absolute value in a list of integers.

      Equations
      Instances For