English
If every π(i) is atomistic, then the Pi-product ∀ i, π(i) is atomistic.
Русский
Если каждый π(i) атомистичен, то произведение Pi ∀ i, π(i) атомистично.
LaTeX
$$$ IsAtomistic\left(\forall i,\ π(i)\right) $$$
Lean4
instance isAtomistic [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)] [∀ i, IsAtomistic (π i)] : IsAtomistic (∀ i, π i)
where
isLUB_atoms
s := by
classical
refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩
rw [isLUB_pi]
intro i
simp_rw [isAtom_iff_eq_single]
refine ⟨?_, ?_⟩
· rintro _ ⟨_, ⟨⟨_, _, _, rfl⟩, hs⟩, rfl⟩
exact hs i
· refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩
