Source indexedlemma · leanprover/lean4:v4.32.0

BohrSet.ext_width

APAP.Prereqs.Bohr.Basic · APAP/Prereqs/Bohr/Basic.lean:67 to 80

Mathematical statement

Exact Lean statement

@[ext]
lemma ext_width {B B' : BohrSet G} (freq : B.frequencies = B'.frequencies)
    (width : ∀ ψ : AddChar G ℂ, ψ ∈ B.frequencies → B.width ψ = B'.width ψ) :
    B = B'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[ext]lemma ext_width {B B' : BohrSet G} (freq : B.frequencies = B'.frequencies)    (width : ∀ ψ : AddChar G ℂ, ψ ∈ B.frequencies → B.width ψ = B'.width ψ) :    B = B' := by  ext  case frequencies => rw [freq]  case ewidth ψ =>    by_cases hψ : ψ ∈ B.frequencies    case pos =>      rw [←coe_width hψ, width _ hψ, coe_width]      rwa [←freq]    case neg =>      rw [ewidth_eq_top_of_not_mem_frequencies hψ, ewidth_eq_top_of_not_mem_frequencies]      rwa [←freq]