coe_inf — Mathlib

English

The carrier of the infimum of two nonunital subsemirings is the intersection of their carriers.

Русский

Носитель наименьшего элемента двух подполуг образует пересечение носителей.

LaTeX

$$coe_inf (p p' : NonUnitalSubsemiring R) : ((p ⊓ p' : NonUnitalSubsemiring R) : Set R) = (p : Set R) ∩ p'$$

Lean4

@[simp]
theorem coe_inf (p p' : NonUnitalSubsemiring R) : ((p ⊓ p' : NonUnitalSubsemiring R) : Set R) = (p : Set R) ∩ p' :=
  rfl

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