mem_map'

Mathlib.Data.Finset.Image

URI: https://scilib.ai/kg/mathlib#Finset.mem_map'

English

The membership of f a in s.map f is equivalent to a ∈ s.

Русский

Членство f a в s.map f эквивалентно a ∈ s.

LaTeX

$$$ f a \in s.map f \iff a \in s $$$

Lean4

@[simp 1100]
theorem mem_map' (f : α ↪ β) {a} {s : Finset α} : f a ∈ s.map f ↔ a ∈ s :=
  mem_map_of_injective f.2

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

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

Разделы

Аффилиация

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