finsetSup_mem_iff — Mathlib

English

Equality form for finset sup with memberships; equivalent to previous statement.

Русский

Эквивалентность для объединения по финсетам и принадлежности.

LaTeX

$$Eq (t.mem (s.sup f)) (∀ i ∈ s, f i ∈ t)$$

Lean4

@[simp]
theorem finsetSup_mem_iff {P : Type*} [SemilatticeSup P] [OrderBot P] (t : Ideal P) {ι : Type*} {f : ι → P}
    {s : Finset ι} : s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t := by classical induction s using Finset.induction_on <;> simp [*]

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