English
InfPrime a is equivalent to InfIrred a in the distributive lattice.
Русский
InfPrime a эквивалентен InfIrred a в распределительной решётке.
LaTeX
$$$\InfPrime a \iff \InfIrred a$$$
Lean4
theorem map_isLUB (hf : IsNormal f) {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) : IsLUB (f '' s) (f a) :=
by
refine ⟨?_, fun b hb ↦ ?_⟩
· simpa [mem_upperBounds, hf.strictMono.le_iff_le] using hs.1
· by_cases ha : a ∈ s
· simp_all [mem_upperBounds]
· have ha' := hs.isSuccLimit_of_notMem hs' ha
rw [le_iff_forall_le hf ha']
intro c hc
obtain ⟨d, hd, hcd, hda⟩ := hs.exists_between hc
simp_rw [mem_upperBounds, forall_mem_image] at hb
exact (hf.strictMono hcd).le.trans (hb hd)
