mem_preimage — Mathlib

English

Same as Image membership; membership in the image is equivalent to the existential condition.

Русский

То же самое, что и членство в образе: принадлежность образу эквивалентна существованию элемента в исходном множестве.

LaTeX

$$b ∈ R.image\,s \iff ∃ a ∈ s, a ~[R] b$$

Lean4

@[simp]
theorem mem_preimage : a ∈ preimage R t ↔ ∃ b ∈ t, a ~[R] b :=
  .rfl

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