instRelHomClass — Mathlib

English

Sum.inr is a relation embedding from s into Sum.Lex r s; for all a,b we have Sum.Lex r s (Sum.inr a) (Sum.inr b) iff s a b.

Русский

Sum.inr — вложение по отношению от s к Sum.Lex r s; для всех a,b выполняется Sum.Lex r s (Sum.inr a) (Sum.inr b) ⇔ s a b.

LaTeX

$$$$ Sum.inr : s \\hookrightarrow_r Sum.Lex r s \\, \\forall a,b,\\; Sum.Lex r s (Sum.inr a) (Sum.inr b) \\iff s\\,a\\,b. $$$$

Lean4

instance : RelHomClass (r ≃r s) r s where map_rel f _ _ := Iff.mpr (map_rel_iff' f)

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