codisjoint_iff — Mathlib

English

Let f,g : ∀ i, α'i with order tops. Then Codisjoint f g holds iff ∀ i, Codisjoint (f i) (g i).

Русский

Пусть f,g : ∀ i, α'i с верхними пределами. Тогда Codisjoint f g эквивалентно ∀ i, Codisjoint (f i) (g i).

LaTeX

$$$\mathrm{Codisjoint}(f,g) \ \Longleftrightarrow \ \forall i,\ \mathrm{Codisjoint}(f(i), g(i)).$$$

Lean4

theorem codisjoint_iff [∀ i, OrderTop (α' i)] {f g : ∀ i, α' i} : Codisjoint f g ↔ ∀ i, Codisjoint (f i) (g i) :=
  @disjoint_iff _ (fun i => (α' i)ᵒᵈ) _ _ _ _

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