mem_seq_iff — Mathlib

English

b ∈ seq s t iff there exists f ∈ s and a ∈ t with f(a) = b.

Русский

b ∈ seq s t тогда и только тогда, когда существует f ∈ s и a ∈ t такие, что f(a) = b.

LaTeX

$$$$ b \\in \\operatorname{seq}(s,t) \\iff \\exists f \\in s, \\exists a \\in t, f(a) = b $$$$

Lean4

@[simp, grind =]
theorem mem_seq_iff {s : Set (α → β)} {t : Set α} {b : β} : b ∈ seq s t ↔ ∃ f ∈ s, ∃ a ∈ t, (f : α → β) a = b :=
  Iff.rfl

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