congr

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.BijOn.congr

English

Repeat of the range subset property for bijective on s t.

Русский

Повторение свойства подмножества образа для биекции на s→t.

LaTeX

$$$\\text{BijOn}(f,s,t)\\Rightarrow t\\subseteq\\operatorname{range}(f)$$$

Lean4

theorem congr (h₁ : BijOn f₁ s t) (h : EqOn f₁ f₂ s) : BijOn f₂ s t :=
  BijOn.mk (h₁.mapsTo.congr h) (h₁.injOn.congr h) (h₁.surjOn.congr h)

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

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

Разделы

Аффилиация

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