refl_left

Mathlib.Data.Prod.Basic

URI: https://scilib.ai/kg/mathlib#Prod.Lex.refl_left

English

If IsRefl α r, then every x ∈ α × β satisfies Prod.Lex r s x x.

Русский

Если IsRefl α r, то для каждого x ∈ α × β имеет Prod.Lex r s x x.

LaTeX

$$$\\\\forall {α} {β} {r} {s} [IsRefl α r], \\\\forall x, Prod.Lex r s x x.$$$

Lean4

@[refl]
theorem refl_left (r : α → α → Prop) (s : β → β → Prop) [IsRefl α r] : ∀ x, Prod.Lex r s x x
  | (_, _) => Lex.left _ _ (refl _)

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

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

Разделы

Аффилиация

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