fixingSubgroup_antitone — Mathlib

English

The map sending a subgroup H of Aut_F(E) to its fixed field E^H is order-reversing: if H1 ⊆ H2, then E^{H2} ⊆ E^{H1}.

Русский

Отображение подгруппы фиксирующих автоматизмов в фиксированное подполе антимонотонно: если H1 ⊆ H2, то E^{H2} ⊆ E^{H1}.

LaTeX

$$$\text{Antitone}(\,\text{fixingSubgroup}\,)$$$

Lean4

theorem fixingSubgroup_antitone : Antitone (@fixingSubgroup F _ E _ _) := fun _ _ ↦ fixingSubgroup_le

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