trans_eq_some — Mathlib

English

Composition of pseudoequivalences maps to some value exactly when there exists a middle value that maps through both parts to that value.

Русский

Компоновка псевдоэквивалентностей выводит некоторый результат тогда и только тогда, когда существует средний элемент, который через обе части отображается в данный результат.

LaTeX

$$$$ f.trans g a = \\text{some } c \\iff \\exists b, f(a)=\\text{some } b \\land g(b)=\\text{some } c. $$$$

Lean4

theorem trans_eq_some (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ) :
    f.trans g a = some c ↔ ∃ b, f a = some b ∧ g b = some c :=
  Option.bind_eq_some_iff

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