semiconj_conj

Mathlib.Logic.Equiv.Basic

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

English

Given an equivalence e: α ≃ β and a function f: α → α, one has Semiconj e f (e.conj f).

Русский

Пусть e: α ≃ β и f: α → α; тогда выполняется semiconj e f (e.conj f).

LaTeX

$$$\\text{Semiconj } e f (e.conj f)$$$

Lean4

theorem semiconj_conj (f : α₁ → α₁) : Semiconj e f (e.conj f) := fun x => by simp

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

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

Разделы

Аффилиация

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