instLE_mathlib

Mathlib.Data.Setoid.Basic

URI: https://scilib.ai/kg/mathlib#Setoid.instLE_mathlib

Lean4

/-- Defining `≤` for equivalence relations. -/
instance : LE (Setoid α) :=
  ⟨fun r s => ∀ ⦃x y⦄, r x y → s x y⟩

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

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

Разделы

Аффилиация

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