exists_inter_eq_singleton — Mathlib

English

If hrep represents s for C, and c ∈ C, then s ∩ c.supp is a singleton: there exists a ∈ V with s ∩ c.supp = {a}.

Русский

Если hrep представляет s для C и c ∈ C, то s ∩ c.supp является синглтоном: существует a, такое что s ∩ c.supp = {a}.

LaTeX

$$$ \\exists a, s \\cap c.supp = \\{ a \\} $$$

Lean4

theorem exists_inter_eq_singleton (hrep : Represents s C) (h : c ∈ C) : ∃ x, s ∩ c.supp = { x } :=
  by
  obtain ⟨a, ha⟩ := existsUnique_rep hrep h
  aesop

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