Setoid - pogi-log

Setoid

Setoid(セトイド)

ある集合$ S と、二項関係の演算子であり同値関係の演算子である「$ \sim 」があって、集合$ S の中身は同値関係であることを満たすような元である構造

同値関係は以下のようなやつ

反射律: $ a ∼ a .

対称律: $ a ∼ b \implies b ∼ a .

推移律: $ a ∼ b \land b ∼ c \implies a ∼ c .

$ \mathrm{Setoid} := (S, \sim)

Leanの場合の定義

LeanではSetoid用の演算子として≈($ \approx )を使う

確認用

Q. Setoid