mem_gen — Mathlib

English

For any V ⊆ β × β, (f,g) ∈ UniformFun.gen α β V if and only if ∀ x, (f x, g x) ∈ V.

Русский

Для любых V ⊆ β × β верно: (f,g) ∈ UniformFun.gen α β V тогда и только тогда, когда ∀ x, (f(x), g(x)) ∈ V.

LaTeX

$$$$(f,g) \in UniformFun.gen(α,β,V) \iff \forall x, (f(x),g(x)) \in V.$$$$

Lean4

@[simp]
protected theorem mem_gen {β} {f g : α →ᵤ β} {V : Set (β × β)} :
    (f, g) ∈ UniformFun.gen α β V ↔ ∀ x, (toFun f x, toFun g x) ∈ V :=
  .rfl

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