supp_eq — Mathlib

English

The support of x is exactly the set of u such that for all representations a, f with abs ⟨a, f⟩ = x, u ∈ f''univ.

Русский

Поддержка x состоит ровно из тех u, для которых для всех представлений a, f с abs ⟨a, f⟩ = x, выполняется u ∈ f''univ.

LaTeX

$$$$\forall {F : Type u \to Type v} [q : QPF F] {\alpha : Type u} (x : F \alpha) , supp x = {u | \forall a f, abs ⟨a, f⟩ = x \rightarrow u \in f '' univ}.$$$$

Lean4

theorem supp_eq {α : Type u} (x : F α) : supp x = {u | ∀ a f, abs ⟨a, f⟩ = x → u ∈ f '' univ} :=
  by
  ext
  apply mem_supp

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