isCompl_coe

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Complementeds.isCompl_coe

English

IsCompl is preserved by the coercion: IsCompl(a.val, b) iff IsCompl(a,b).

Русский

IsCompl сохраняется через вложение: IsCompl(a.val, b) эквивалентно IsCompl(a,b).

LaTeX

$$$\forall a,b\in \mathrm{Complementeds}(\alpha),\ IsCompl(a.\mathrm{val}, b) \iff IsCompl(a,b).$$$

Lean4

@[simp, norm_cast]
theorem isCompl_coe : IsCompl (a : α) b ↔ IsCompl a b := by simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru