mem_trans — Mathlib

English

Membership in the transitive combination f.trans g a is characterized by the existence of an intermediate b with b in f a and c in g b.

Русский

Принадлежность элемента к составному отображению f.trans g a описывается существованием промежуточного b, такого что b ∈ f a и c ∈ g b.

LaTeX

$$$$ c \\in (f\\,\\trans\\, g)\\ a \\iff \\exists b, b \\in f(a) \\land c \\in g(b). $$$$

Lean4

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

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