prehaar_mono — Mathlib

English

If K1 ⊆ K2, then prehaar(K0, U, K1) ≤ prehaar(K0, U, K2).

Русский

Если K1 ⊆ K2, то prehaar(K0,U,K1) ≤ prehaar(K0,U,K2).

LaTeX

$$$\text{prehaar}_{K_0}(U, K_1) \le \text{prehaar}_{K_0}(U, K_2)\quad(K_1 \subseteq K_2)$$$

Lean4

@[to_additive]
theorem prehaar_mono {K₀ : PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty) {K₁ K₂ : Compacts G}
    (h : (K₁ : Set G) ⊆ K₂.1) : prehaar (K₀ : Set G) U K₁ ≤ prehaar (K₀ : Set G) U K₂ :=
  by
  simp only [prehaar]; rw [div_le_div_iff_of_pos_right]
  · exact mod_cast index_mono K₂.2 h hU
  · exact mod_cast index_pos K₀ hU

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