minimal_apply_mem_iff — Mathlib

English

Under subset condition, minimal in t maps to minimal in the domain via the embedding is equivalent to a membership equivalence.

Русский

При условии подмножества минимальное в t отображается в минимальное на домене через вложение, взаимно эквивалентно по членству.

LaTeX

$$$\\forall ht:\\; t \\subseteq \\operatorname{range}f,\\; \\big( \\text{Minimal}(\\cdot \\in t) (f x) \\iff \\text{Minimal}(\\cdot \\in t) x \\big) $$$

Lean4

theorem minimal_apply_mem_iff (ht : t ⊆ Set.range f) : Minimal (· ∈ t) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x := by
  rw [← f.minimal_apply_mem_inter_range_iff, inter_eq_self_of_subset_left ht]

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