codisjoint_inf_right

Mathlib.Data.Finset.Lattice.Fold

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

English

Codisjoint a (s.inf f) iff ∀ i ∈ s, Codisjoint a (f i).

Русский

Коодисjoint a (s.inf f) эквивалентно ∀ i ∈ s, Codisjoint a (f i).

LaTeX

$$$ Codisjoint a (s.\\inf f) \\iff \\forall i, i \\in s \\rightarrow Codisjoint a (f i) $$$

Lean4

protected theorem codisjoint_inf_right : Codisjoint a (s.inf f) ↔ ∀ ⦃i⦄, i ∈ s → Codisjoint a (f i) :=
  @Finset.disjoint_sup_right αᵒᵈ _ _ _ _ _ _

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

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

Разделы

Аффилиация

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