English
The composite is none exactly when, for all b,c, either b is not in f a or c is not in g b.
Русский
Композиция равна none тогда и только тогда, когда для всех b,c верно, что либо b не принадлежит f a, либо c не принадлежит g b.
LaTeX
$$$$ f.trans g a = \\text{none} \\iff \\forall b c, b \\notin f a \\lor c \\notin g b. $$$$
Lean4
theorem trans_eq_none (f : α ≃. β) (g : β ≃. γ) (a : α) : f.trans g a = none ↔ ∀ b c, b ∉ f a ∨ c ∉ g b :=
by
simp only [eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm]
push_neg
exact forall_swap