eq_iff

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.InjOn.eq_iff

English

If f is injOn on s, then for any x,y in s, f x = f y iff x = y.

Русский

Если f инъективна на s, то для любых x,y ∈ s верно f x = f y ↔ x = y.

LaTeX

$$$\\\\InjOn f s \\\\rightarrow \\\\forall x,y \\\\in s, f x = f y \\\\leftrightarrow x = y$$$

Lean4

theorem eq_iff {x y} (h : InjOn f s) (hx : x ∈ s) (hy : y ∈ s) : f x = f y ↔ x = y :=
  ⟨h hx hy, fun h => h ▸ rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru