image_inter

Mathlib.Data.Finset.Image

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

← MathLib Explorer

English

If f is injective, then (s1 ∩ s2).image f = s1.image f ∩ s2.image f.

Русский

Если f инъективна, то (s1 ∩ s2).image f = s1.image f ∩ s2.image f.

LaTeX

$$$\text{Injective } f \Rightarrow (s_1 \cap s_2).image f = s_1.image f \cap s_2.image f$$$

Lean4

theorem image_inter [DecidableEq α] (s₁ s₂ : Finset α) (hf : Injective f) :
    (s₁ ∩ s₂).image f = s₁.image f ∩ s₂.image f :=
  image_inter_of_injOn _ _ hf.injOn

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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