instIsRelIffMk' — Mathlib

English

The IsRelIff property holds for the constructed embedding mk' with its accompanying data iff the generating iff holds.

Русский

Свойство IsRelIff сохраняется для сконструированного вложения mk' с соответствующими данными тогда и только тогда, когда выполняется эквивалентное условие.

LaTeX

$$$ (\\text{mk' } c\\; c'\\; f\\; hf\\; iff).IsRelIff $$$

Lean4

instance : (mk' c c' f hf iff).IsRelIff where rel' _ _ h := (iff _ _).2 h

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