preimage_subset

Mathlib.Data.Set.Image

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

← MathLib Explorer

English

If f is injective and t is a surjective image of s, then f^{-1}(t) ⊆ s.

Русский

Если f инъективна и t является образом s по f, то f^{-1}(t) ⊆ s.

LaTeX

$$f is injective ∧ t = f''s ⇒ f^{-1}(t) ⊆ s$$

Lean4

theorem preimage_subset {s t} (hs : s ⊆ f '' t) (hf : Set.InjOn f (f ⁻¹' s)) : f ⁻¹' s ⊆ t :=
  by
  rintro a ha
  obtain ⟨b, hb, hba⟩ := hs ha
  rwa [hf ha _ hba.symm]
  simpa [hba]

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

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

Разделы

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

Аффилиация

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