English
The product over a finite set of elements in pairwise distinct Archimedean classes lies in the lowest class; more precisely, if s is a nonempty finite set and a_i : i → M is a family such that mk(a_i) are pairwise distinct and mk ∘ a is strictly monotone on s, then mk(∏_{i∈s} a_i) = mk(a_{min}), where min is taken in the order of s.
Русский
Произведение по конечному множеству элементов из попарно различных Архимедовых классов лежит в нижшем классе; точнее, если s ненулевой непустой конечный набор и семейство a_i : i → M таково, что mk(a_i) попарно различны, и mk ∘ a строго монотонно на s, то mk(∏_{i∈s} a_i) = mk(a_{min}), где min выбирается по порядку на s.
LaTeX
$$\text{mk}\left(\prod_{i \in s} a_i\right) = mk\left(a\left( s.min' hnonempty \right)\right)$$
Lean4
/-- The product over a set of an elements in distinct classes is in the lowest class. -/
@[to_additive /-- The sum over a set of an elements in distinct classes is in the lowest class. -/
]
theorem mk_prod {ι : Type*} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M} :
StrictMonoOn (mk ∘ a) s → mk (∏ i ∈ s, (a i)) = mk (a (s.min' hnonempty)) := by
induction hnonempty using Finset.Nonempty.cons_induction with
| singleton i => simp
| cons i s hi hs ih =>
intro hmono
obtain ih := ih (hmono.mono (by simp))
rw [Finset.prod_cons]
have hminmem : s.min' hs ∈ (Finset.cons i s hi) := Finset.mem_cons_of_mem (Finset.min'_mem _ _)
have hne : mk (a i) ≠ mk (a (s.min' hs)) := by
by_contra!
obtain eq := hmono.injOn (by simp) hminmem this
rw [eq] at hi
exact hi (Finset.min'_mem _ hs)
rw [← ih] at hne
obtain hlt | hlt := lt_or_gt_of_ne hne
· rw [mk_mul_eq_mk_left hlt]
congr
apply le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ (by simp))
intro y hy
obtain rfl | hmem := Finset.mem_cons.mp hy
· rfl
· refine (lt_of_lt_of_le ?_ (Finset.min'_le _ _ hmem)).le
apply (hmono.lt_iff_lt (by simp) hminmem).mp
rw [ih] at hlt
exact hlt
· rw [mul_comm, mk_mul_eq_mk_left hlt, ih]
congr 2
refine le_antisymm (Finset.le_min' _ _ _ ?_) (Finset.min'_le _ _ hminmem)
intro y hy
obtain rfl | hmem := Finset.mem_cons.mp hy
· apply ((hmono.lt_iff_lt hminmem (by simp)).mp ?_).le
rw [ih] at hlt
exact hlt
· exact Finset.min'_le _ _ hmem
