coe_inf — Mathlib

English

The underlying set of the infimum of two intermediate fields is exactly the intersection of their underlying sets.

Русский

Подмножество инфимума двух промежуточных полей равно пересечению их соответствующих множеств.

LaTeX

$$$ (\\uparrow (S \\cap T) : \\mathrm{Set} E) = (S : \\mathrm{Set} E) \\cap (T : \\mathrm{Set} E) $$$

Lean4

@[simp, norm_cast]
theorem coe_inf (S T : IntermediateField F E) : (↑(S ⊓ T) : Set E) = (S : Set E) ∩ T :=
  rfl

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