image2_def — Mathlib

English

The image of s under a function f corresponds to the monadic expression: image2 f s t = f <$> s <*> t.

Русский

Образ множества s под функцией f эквивалентен монадическому выражению: image2 f s t = f <$> s <*> t.

LaTeX

$$$\mathrm{image2}(f, s, t) = f \langle\cdot\rangle s \\<* > t$$$

Lean4

/-- `Set.image2` in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism. -/
theorem image2_def {α β γ : Type u} (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = f <$> s <*> t :=
  by
  ext
  simp

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