inverse_apply_eq — Mathlib

English

If f x = y for x ∈ domain and y ∈ inverse.domain, then inverse y = x.

Русский

Если f x = y для x из области определения и y принадлежит области определения обратного, тогда обратное y равно x.

LaTeX

$$∀ x ∈ domain(f), f x = y ⇒ (inverse f) y = x$$

Lean4

theorem inverse_apply_eq {y : (inverse f).domain} {x : f.domain} (hxy : f x = y) : (inverse f) y = x :=
  by
  have := mem_inverse_graph hf x
  grind [mem_graph_iff]

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