bijOn_symm

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Equiv.bijOn_symm

English

For any e: α ≃ β and sets s ⊆ α, t ⊆ β, bijOn e.symm t s is equivalent to bijOn e s t.

Русский

Для любых e: α ≃ β и множеств s ⊆ α, t ⊆ β верно, что bijOn e^{-1} t s эквивалентно bijOn e s t.

LaTeX

$$$\mathrm{BijOn}(e^{\,-1}, t, s) \iff \mathrm{BijOn}(e, s, t)$$$

Lean4

@[simp]
theorem bijOn_symm : BijOn e.symm t s ↔ BijOn e s t :=
  bijOn_comm e.symm.invOn

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

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

Разделы

Аффилиация

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