single_trans_of_eq_none

Mathlib.Data.PEquiv

URI: https://scilib.ai/kg/mathlib#PEquiv.single_trans_of_eq_none

← MathLib Explorer

English

Repeated version: If f.symm b = none, then f.trans (single b c) = ⊥.

Русский

Повторяющаяся версия: Если f.symm b = none, то f.trans (single b c) = ⊥.

LaTeX

$$f.symm b = None \Rightarrow f.trans (single b c) = \bot$$

Lean4

theorem single_trans_of_eq_none (a : α) {b : β} {f : β ≃. δ} (h : f b = none) : (single a b).trans f = ⊥ :=
  symm_injective <| trans_single_of_eq_none _ h

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

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

Разделы

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

Аффилиация

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