Theorems · Theorem · Lie groups

RestrictedProduct.inclusion.congr_simp

∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖)
  (x x_1 : RestrictedProduct (fun i => R i) (fun i => A i) 𝓖),
  x = x_1 → RestrictedProduct.inclusion R A h x = RestrictedProduct.inclusion R A h x_1

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound