monotone — Mathlib

English

If S ≤ S′, then the corresponding Selmer groups satisfy K⟮S,n⟯ ≤ K⟮S′,n⟯; enlarging the set of places relaxes the local conditions.

Русский

Если S ≤ S′, то соответствующие группы Selmer удовлетворяют K⟮S,n⟯ ≤ K⟮S′,n⟯; расширение множества мест ослабляет локальные условия.

LaTeX

$$S ≤ S' ⇒ K⟮S,n⟯ ≤ K⟮S',n⟯$$

Lean4

theorem monotone (hS : S ≤ S') : K⟮S,n⟯ ≤ K⟮S',n⟯ := fun _ hx v => hx v ∘ mt (@hS v)

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