instFunLike — Mathlib

English

If α has a preorder, then ClosureOperator(α) carries a FunLike structure, i.e., each closure operator acts as a function α → α with appropriate coherence.

Русский

Если у α имеется предорядок, то ClosureOperator(α) обладает структурой FunLike, то есть каждый замыкатель действует как функция α → α с необходимой согласованностью.

LaTeX

$$ [Preorder α] ⇒ FunLike(ClosureOperator α, α, α)$$

Lean4

instance [Preorder α] : FunLike (ClosureOperator α) α α
    where
  coe c := c.1
  coe_injective' := by rintro ⟨⟩ ⟨⟩ h; obtain rfl := DFunLike.ext' h; congr with x; simp_all

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