ne_iff

Mathlib.Data.Set.Function

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

English

If f is injOn on s, then f x ≠ f y iff x ≠ y for x,y ∈ s.

Русский

Если f инъективна на s, то f x ≠ f y эквивалентно x ≠ y для x,y ∈ s.

LaTeX

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

Lean4

theorem ne_iff {x y} (h : InjOn f s) (hx : x ∈ s) (hy : y ∈ s) : f x ≠ f y ↔ x ≠ y :=
  (h.eq_iff hx hy).not

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

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

Разделы

Аффилиация

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