English
Let f,g : ∀ i, α'i with each α'i a poset. Then Disjoint f g holds iff ∀ i, Disjoint (f i) (g i).
Русский
Пусть f,g : ∀ i, α'i, где каждый α'i — частично упорядоченное множество. Тогда Disjoint f g эквивалентно ∀ i, Disjoint (f i) (g i).
LaTeX
$$$\mathrm{Disjoint}(f,g) \ \Longleftrightarrow \ \forall i,\ \mathrm{Disjoint}(f(i), g(i)).$$$
Lean4
theorem disjoint_iff [∀ i, OrderBot (α' i)] {f g : ∀ i, α' i} : Disjoint f g ↔ ∀ i, Disjoint (f i) (g i) := by
classical
constructor
· intro h i x hf hg
exact
(update_le_iff.mp <| h (update_le_iff.mpr ⟨hf, fun _ _ => bot_le⟩) (update_le_iff.mpr ⟨hg, fun _ _ => bot_le⟩)).1
· intro h x hf hg i
apply h i (hf i) (hg i)
