genWeightSpaceOf_ne_bot — Mathlib

English

For every χ and x ∈ L, the generalized χ-weight space at x is nontrivial: genWeightSpaceOf M (χ x) x ≠ ⊥.

Русский

Для каждого χ и x ∈ L обобщённое весовое пространство χ(x) при x не тривиально: genWeightSpaceOf M (χ x) x ≠ ⊥.

LaTeX

$$genWeightSpaceOf M (χ x) x ≠ ⊥$$

Lean4

theorem genWeightSpaceOf_ne_bot (χ : Weight R L M) (x : L) : genWeightSpaceOf M (χ x) x ≠ ⊥ :=
  by
  have : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥ := χ.genWeightSpace_ne_bot
  contrapose! this
  rw [eq_bot_iff]
  exact le_of_le_of_eq (iInf_le _ _) this

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