English
In the dual situation to 165542, with order duals and WellFoundedGT assumptions, the lattice α is Noetherian under the corresponding hypotheses.
Русский
В двойственной постановке к 165542, при использовании соответствующих условий для GT-порядка, решетка α является Noetherian при заданных гипотезах.
LaTeX
$$$\text{If the dual assumptions of 165542 hold (i.e., dual order and WellFoundedGT), then }\mathrm{WellFoundedGT}(\alpha).$$$
Lean4
/-- A generalization of the theorem that if `N` is a submodule of `M` and
`N` and `M / N` are both Noetherian, then `M` is Noetherian. -/
theorem wellFounded_gt_exact_sequence {β γ : Type*} [Preorder β] [Preorder γ] [WellFoundedGT β] [WellFoundedGT γ]
(K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ) (gci : GaloisCoinsertion f₁ f₂)
(gi : GaloisInsertion g₂ g₁) (hf : ∀ a, f₁ (f₂ a) = a ⊓ K) (hg : ∀ a, g₁ (g₂ a) = a ⊔ K) : WellFoundedGT α :=
wellFounded_lt_exact_sequence (α := αᵒᵈ) (β := γᵒᵈ) (γ := βᵒᵈ) K g₁ g₂ f₁ f₂ gi.dual gci.dual hg hf
