infIrred_iff_of_finite — Mathlib

English

For a finite α, InfIrred s is equivalent to s = Ici a for some a.

Русский

Для конечного α InfIrred s эквивалентно тому, что s = Ici a для некоторого a.

LaTeX

$$InfIrred s \leftrightarrow \exists a, Ici(a) = s$$

Lean4

@[simp]
theorem infIrred_iff_of_finite : InfIrred s ↔ ∃ a, Ici a = s :=
  by
  refine ⟨fun hs ↦ ?_, ?_⟩
  · obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_minimal (coe_nonempty.2 hs.ne_top)
    exact
      ⟨a, (hs.2 <| erase_inf_Ici ha fun b hb ↦ le_imp_eq_iff_le_imp_ge.2 <| has hb).resolve_left (lt_erase.2 ha).ne'⟩
  · rintro ⟨a, rfl⟩
    exact infIrred_Ici _

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