le_set' — Mathlib

English

A variant of le_set with a mapping g: α → Ordinal, reducing p via image under g.

Русский

Вариант леммы le_set с отображением g: α → Ordinal, который переносит множество p через образ g.

LaTeX

$$$\forall f\,\bigl(\mathrm{IsNormal}(f)\bigr)\; \forall p\; (p\neq \emptyset)\; \forall (g : \alpha \to \mathrm{Ordinal})\; (b)\; (\forall o, b \le o \iff \forall a \in p, g(a) \le o) \to (f(b) \le o \iff \forall a \in p, f(g(a)) \le o).$$$

Lean4

theorem le_set' {f o} (H : IsNormal f) (p : Set α) (p0 : p.Nonempty) (g : α → Ordinal) (b)
    (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, g a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o := by
  simpa [H₂] using H.le_set (g '' p) (p0.image g) b

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