preimage_subset

Mathlib.Data.Finset.Preimage

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

← MathLib Explorer

English

If s ⊆ t.map f for an embedding f, then s.preimage ⊆ t.

Русский

Если s ⊆ t.map f, то s.preimage ⊆ t.

LaTeX

$$$$ s \\subseteq t.map f \\Rightarrow s.preimage f f.injective.injOn \\subseteq t. $$$$

Lean4

theorem preimage_subset {f : α ↪ β} {s : Finset β} {t : Finset α} (hs : s ⊆ t.map f) :
    s.preimage f f.injective.injOn ⊆ t := fun _ h => (mem_map' f).1 (hs (mem_preimage.1 h))

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

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

Разделы

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

Аффилиация

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