mk' — Mathlib

English

A criterion for IsUniformInducing given a family of sets controlling preimage behavior; if h provides the equivalence of neighborhoods via t in β, then f is IsUniformInducing.

Русский

Критерий для IsUniformInducing по семейству множеств, контролирующему поведение предобразов; если h задаёт эквивалентность окрестностей, то f — IsUniformInducing.

LaTeX

$$$\\langle h \\rangle \\Rightarrow IsUniformInducing f$$$

Lean4

theorem mk' {f : α → β} (h : ∀ s, s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ x y : α, (f x, f y) ∈ t → (x, y) ∈ s) : IsUniformInducing f :=
  ⟨by simp [eq_comm, Filter.ext_iff, subset_def, h]⟩

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