normal_inf — Mathlib

English

The infimum (intersection) of two normal extensions is normal.

Русский

Нижняя граница (пересечение) двух нормальных расширений нормальна.

LaTeX

$$Normal F (E ⊓ E' : IntermediateField F K)$$

Lean4

@[stacks 09HP]
instance normal_inf (E E' : IntermediateField F K) [Normal F E] [Normal F E'] :
    Normal F (E ⊓ E' : IntermediateField F K) :=
  iInf_bool_eq (f := Bool.rec E' E) ▸ normal_iInf (h := by rintro (_ | _) <;> infer_instance)

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