fixingSubgroup_le — Mathlib

English

The map H ↦ fixingSubgroup H is antitone: larger H gives smaller fixingSubgroup.

Русский

Отображение H ↦ fixingSubgroup(H) антимонотонно: чем больше H, тем меньше fixingSubgroup.

LaTeX

$$Antitone fixingSubgroup$$

Lean4

/-- The map `K ↦ Gal(E/K)` is inclusion-reversing. -/
theorem fixingSubgroup_le {K1 K2 : IntermediateField F E} (h12 : K1 ≤ K2) : K2.fixingSubgroup ≤ K1.fixingSubgroup :=
  fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h12 hx⟩

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