sup_carrier_def — Mathlib

English

The carrier of the supremum J ⊔ J' is the carrier of the maximum element, i.e., the carrier of the join equals the join of carriers.

Русский

Носитель наибольшего элемента J ⊔ J' равен носителю их объединения; носитель объединения равен объединению носителей.

LaTeX

$$$(J \sqcup J').carrier = J \sqcup J'$$

Lean4

theorem sup_carrier_def (J J' : SubDPIdeal hI) : (J ⊔ J').carrier = J ⊔ J' :=
  rfl

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