L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
a b : M
⊢ RelMap leSymb ![a, b] ↔ a ≤ b
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
a b : M
⊢ RelMap leSymb ![a, b] ↔ a ≤ b
rw [← orderLHom_leSymb, LHom.map_onRelation]
no goals
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
a b : M
⊢ RelMap leSymb ![a, b] ↔ a ≤ b
rfl