cons_ne — Mathlib

English

The value of Pi.cons at an argument a' that lies in a :: m is the same as applying the function to a' using the witness from the appropriate membership clause when a' ≠ a.

Русский

Значение Pi.cons в точке a' внутри a :: m равно значению функции в a' с учётом свидетеля принадлежности, когда a' ≠ a.

LaTeX

$$$\\Pi\\text{-cons}(m,a, b, f)\\ a' = f\\ a'\\ ((mem\\_cons.1\\ h').resolve\\_left\\ h).$$$

Lean4

theorem cons_ne {a a' : α} {b : δ a} {f : ∀ a ∈ m, δ a} (h' : a' ∈ a ::ₘ m) (h : a' ≠ a) :
    Pi.cons m a b f a' h' = f a' ((mem_cons.1 h').resolve_left h) :=
  dif_neg h

Похожие утверждения