map_apply_apply — Mathlib

English

Under injective f and g, Map r f g (f a) (g b) is equivalent to r a b.

Русский

При инъективности f и g, Map r f g (f a) (g b) эквивалентно r a b.

LaTeX

$$$\text{Injective}(f) \to \text{Injective}(g) \to \forall a,b,\; \mathrm{Map}\,r\,f\,g\ (f\,a)\,(g\,b) \iff r\,a\,b$$$

Lean4

@[simp]
theorem map_apply_apply (hf : Injective f) (hg : Injective g) (r : α → β → Prop) (a : α) (b : β) :
    Relation.Map r f g (f a) (g b) ↔ r a b := by simp [Relation.Map, hf.eq_iff, hg.eq_iff]

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