coe_inf — Mathlib

English

The carrier of the infimum of two subfields p and p' equals the intersection of their carriers: ((p ⊓ p' : Subfield K) : Set K) = p.carrier ∩ p'.carrier.

Русский

Носитель наибольшего нижнего предела двух подполь полей p и p' равен пересечению их носителей: ((p ⊓ p' : Subfield K) : Set K) = p.carrier ∩ p'.carrier.

LaTeX

$$$((p \sqcap p' : Subfield K) : Set K) = p.carrier \cap p'.carrier$$$

Lean4

@[simp, norm_cast]
theorem coe_inf (p p' : Subfield K) : ((p ⊓ p' : Subfield K) : Set K) = p.carrier ∩ p'.carrier :=
  rfl

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