Setoid
Setoid(セトイド、亜集合)
ある集合$ S と、二項関係の演算子であり同値関係の演算子である「$ \sim 」があって、集合$ S の中身は同値関係であることを満たすような元である構造 同値関係は以下のようなやつ
対称律: $ a ∼ b \implies b ∼ a . 推移律: $ a ∼ b \land b ∼ c \implies a ∼ c . $ \mathrm{Setoid} := (S, \sim)
Leanの場合の定義
LeanではSetoid用の演算子として≈($ \approx )を使う
確認用
Q. Setoid
関連
参考
メモ
調査用
Wikipedia.icon
Wikipedia.icon