instIsReflLex

Mathlib.Data.Sigma.Lex

URI: https://scilib.ai/kg/mathlib#Sigma.instIsReflLex

English

If each αi has IsRefl under s i, then Lex r s is reflexive on Σ i, α i.

Русский

Если для каждого i выполняется IsRefl (αi) (s i), то Lex r s на Σ i, α i тождественно рефлексивен.

LaTeX

$$$[\\forall i, IsRefl(\\alpha i)(s i)] : IsRefl \\bigl( (i,\\alpha i) \\bigr) (Sigma.Lex r s).$$$

Lean4

instance [∀ i, IsRefl (α i) (s i)] : IsRefl _ (Lex r s) :=
  ⟨fun ⟨_, _⟩ => Lex.right _ _ <| refl _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru