normalClosure_mono — Mathlib

English

If K ≤ K' are intermediate fields, then normalClosure F K L ≤ normalClosure F K' L.

Русский

Если K ≤ K' — промежуточные поля, то нормальное замыкание K в L над F не превосходит нормальное замыкание K' в L над F.

LaTeX

$$$K \le K' \Rightarrow \operatorname{normalClosure} F K L \le \operatorname{normalClosure} F K' L$$$

Lean4

theorem normalClosure_mono (h : K ≤ K') : normalClosure F K L ≤ normalClosure F K' L :=
  by
  rw [normalClosure_def', normalClosure_def']
  exact iSup_mono (fun f ↦ map_mono f h)

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