infIrred — Mathlib

English

In a semilattice with inf, if an element a is InfPrime, then it is InfIrred; i.e., a prime element is irreducible with respect to inf.

Русский

В полузаданных мат. структурах с операцией Inf, если элемент a является InfPrime, то он InfIrred; то есть простота элемента влечет за собой неразложимость.

LaTeX

$$$$\\text{InfPrime}(a) \\to \\text{InfIrred}(a).$$$$

Lean4

protected theorem infIrred : InfPrime a → InfIrred a :=
  And.imp_right fun h b c ha => by simpa [← ha] using h ha.le

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