restrictPreimage_surjective

Mathlib.Data.Set.Restrict

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

← MathLib Explorer

English

If f is surjective, then t.restrictPreimage f is surjective.

Русский

Если f сюръективна, то t.restrictPreimage f сюръективна.

LaTeX

$$$\text{Surjective}(f) \Rightarrow \text{Surjective}(t.\restrictPreimage f)$$$

Lean4

theorem restrictPreimage_surjective (hf : Surjective f) : Surjective (t.restrictPreimage f) := fun x =>
  ⟨⟨_, ((hf x).choose_spec.symm ▸ x.2 : _ ∈ t)⟩, Subtype.ext (hf x).choose_spec⟩

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

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

Разделы

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

Аффилиация

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