supIrred_iff_of_finite — Mathlib

English

For a finite α, InfIrred s ⇔ ∃ a, Iic a = s.

Русский

Для конечного α InfIrred s эквивалентно существованию a с Iic a = s.

LaTeX

$$InfIrred s ↔ ∃ a, Iic a = s$$

Lean4

@[simp]
theorem supIrred_iff_of_finite : SupIrred s ↔ ∃ a, Iic a = s :=
  by
  refine ⟨fun hs ↦ ?_, ?_⟩
  · obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_maximal (coe_nonempty.2 hs.ne_bot)
    exact
      ⟨a, (hs.2 <| erase_sup_Iic ha fun b hb ↦ le_imp_eq_iff_le_imp_ge'.2 <| has hb).resolve_left (erase_lt.2 ha).ne⟩
  · rintro ⟨a, rfl⟩
    exact supIrred_Iic _

Похожие утверждения