reduce_isSpecial' — Mathlib

English

Let u be an element of XgcdType with IsSpecial. Then the reduced element u.reduce satisfies IsSpecial'. In other words, the special status is preserved by reduction.

Русский

Пусть u — элемент XgcdType, обладающий свойством IsSpecial. Тогда редуцированное состояние u.reduce удовлетворяет IsSpecial'. Иными словами, свойство специальности сохраняется при редукции.

LaTeX

$$$\forall u : XgcdType,\ IsSpecial(u) \rightarrow IsSpecial'(u.reduce)$$$

Lean4

theorem reduce_isSpecial' (u : XgcdType) (hs : u.IsSpecial) : u.reduce.IsSpecial' :=
  (isSpecial_iff _).mp (u.reduce_isSpecial hs)

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