maximalFor_eq_iff — Mathlib

English

For any i, j, f, the statement that i is the maximal input with f i = j is equivalent to i = j.

Русский

Для любых i, j, f утверждение, что i является максимальным аргументом, удовлетворяющим f i = j, эквивалентно i = j.

LaTeX

$$$ \text{MaximalFor}(x \mapsto x = j)\ f\ i \iff i = j $$$

Lean4

@[simp]
theorem maximalFor_eq_iff : MaximalFor (· = j) f i ↔ i = j := by simp +contextual [MaximalFor]

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