isCompl_iff — Mathlib

English

In a Pi-type with bounded orders, IsCompl f g holds iff ∀ i, IsCompl (f i) (g i).

Русский

Для Π‑типа с ограниченными порядками, IsCompl f g эквивалентно ∀ i, IsCompl (f i) (g i).

LaTeX

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

Lean4

theorem isCompl_iff [∀ i, BoundedOrder (α' i)] {f g : ∀ i, α' i} : IsCompl f g ↔ ∀ i, IsCompl (f i) (g i) := by
  simp_rw [_root_.isCompl_iff, disjoint_iff, codisjoint_iff, forall_and]

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