eq_some_iff — Mathlib

English

Composition of pseudoequivalences preserves the property of mapping to some value: f.trans g a = some c iff there exists b with f a = some b and g b = some c.

Русский

Компоновка псевдоэквивалентностей сохраняет отображение в некий элемент: f.trans g a = some c тогда и только тогда, существует b такой, что f a = some b и g b = some c.

LaTeX

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

Lean4

theorem eq_some_iff (f : α ≃. β) : ∀ {a : α} {b : β}, f.symm b = some a ↔ f a = some b :=
  f.3 _ _

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