restrictPreimage_bijective

Mathlib.Data.Set.Restrict

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem restrictPreimage_bijective (hf : Bijective f) : Bijective (t.restrictPreimage f) :=
  ⟨t.restrictPreimage_injective hf.1, t.restrictPreimage_surjective hf.2⟩

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

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

Разделы

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

Аффилиация

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