mem_map_mk

Mathlib.Data.Finset.Image

URI: https://scilib.ai/kg/mathlib#Finset.mem_map_mk

English

For any injective f, f a ∈ s.map ⟨f,hf⟩ iff a ∈ s.

Русский

Для вложения f, f a ∈ s.map ⟨f, hf⟩ тогда и только тогда, когда a ∈ s.

LaTeX

$$$ f a \in s.map \langle f, hf \rangle \iff a \in s $$$

Lean4

@[simp 1100]
theorem mem_map_mk (f : α → β) {a : α} {s : Finset α} (hf : Function.Injective f) : f a ∈ s.map ⟨f, hf⟩ ↔ a ∈ s :=
  Finset.mem_map' _

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

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

Разделы

Аффилиация

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