English
Characterization of PWOn for ProdLex: s is PWOn iff the fst-projection image is PWOn and all fibers are PWOn.
Русский
Характеризация PWOn для ProdLex: s — PWOn тогда и только тогда, когда образ проекции fst и все волокна являются PWOn.
LaTeX
$$s.IsPWO ↔ ((fun x => (fst x)) '' s).IsPWO ∧ ∀ a, {y | toLex (a, y) ∈ s}.IsPWO$$
Lean4
theorem fiberProdLex [Preorder α] [Preorder β] {s : Set (α ×ₗ β)} (hαβ : s.IsPWO) (a : α) :
{y | toLex (a, y) ∈ s}.IsPWO := by
let f : α ×ₗ β → β := fun x => (ofLex x).2
have h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' { a }) :=
by
ext x
simp [f]
rw [h]
apply IsPWO.image_of_monotoneOn (hαβ.mono inter_subset_left)
rintro b ⟨-, hb⟩ c ⟨-, hc⟩ hbc
simp only [mem_preimage, mem_singleton_iff] at hb hc
have : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c := Prod.Lex.toLex_le_toLex.mp hbc
simp_all only [lt_self_iff_false, true_and, false_or]
