Theorems · Theorem · order theory

Std.ge_refl

∀ {α : Type u_1} [inst : LE α] [inst_1 : Std.Refl fun x1 x2 => x1 ≥ x2] (a : α), a ≤ a

A version of Std.le_refl that works with Std.Refl (· ≥ ·). This is needed for to_dual translations because Std.le_refl requires Std.Refl (· ≤ ·), but after translation instReflLe becomes instReflGe : Std.Refl (· ≥ ·).

Defined in

Mathlib.Order.RelClasses

Cited by

23 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

LEStd.Refl