one_notMem_div_iff

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.one_notMem_div_iff

English

(1) ∉ s / t iff Disjoint(s,t).

Русский

(1) не принадлежит s / t тогда и только тогда, когда s и t несовпадающи.

LaTeX

$$(1 ∉ s / t) ⇔ Disjoint(s,t)$$

Lean4

@[to_additive]
theorem one_notMem_div_iff : (1 : α) ∉ s / t ↔ Disjoint s t :=
  one_mem_div_iff.not_left

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

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

Разделы

Аффилиация

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