mono — Mathlib

English

If h is a fundamental domain for G and ν ≪ μ, then ν is a fundamental domain with respect to μ; i.e., h.mono_ac hle implies IsFundamentalDomain for ν.

Русский

Если h — фундаментальная область для G и ν ≪ μ, то ν является фундаментальной областью по отношению к μ; то есть монотонно сохраняются условия.

LaTeX

$$$h.1.mono_ac\\ hle$$$

Lean4

@[to_additive]
theorem mono (h : IsFundamentalDomain G s μ) {ν : Measure α} (hle : ν ≪ μ) : IsFundamentalDomain G s ν :=
  ⟨h.1.mono_ac hle, hle h.2, h.aedisjoint.mono fun _ _ h => hle h⟩

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