prehaar_pos — Mathlib

English

If V has nonempty interior and K is compact, then prehaar(K0, U, K) is positive (strictly greater than 0).

Русский

Если V имеет непустое interior и K компакт, то prehaar(K0,U,K) положительно: > 0.

LaTeX

$$$0 < \text{prehaar}_{K_0}(U, K)$$$

Lean4

@[to_additive]
theorem prehaar_pos (K₀ : PositiveCompacts G) {U : Set G} (hU : (interior U).Nonempty) {K : Set G} (h1K : IsCompact K)
    (h2K : (interior K).Nonempty) : 0 < prehaar (K₀ : Set G) U ⟨K, h1K⟩ :=
  by
  apply div_pos <;> norm_cast
  · apply index_pos ⟨⟨K, h1K⟩, h2K⟩ hU
  · exact index_pos K₀ hU

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