mathlib-unicode

$ grep -o . <<< "αλ→⟨⟩₂₁β←≤∈∀ℕμιℝ∥↔𝕜₀⁻≠⟶¹∃≫γ•∧×≃Πεσ𝓝ℤ₃⊆φ↑ₗ∞≥∘π⥤∑▸∩⊤δ∫∂¬⊓⊥Γ𝟙⊔∣⊗ᶠ∏ℂ∨ν∪⋙≅ℚ⋃∅ᶜₘₐᵥωᵐ⨆⟪⟫∉⊢⦃⦄⨅⁅⁆⊕⇑ᵖτᵒ⟦⟧ϕΣᵢ‹›ₙ₄ₜΦ⋂ψℒ𝕂⬝ö↪η𝓤𝓟𝔸≈ₛ⟮⟯ΨéΛ₊≡↦⟹≪ζᵃ≌√𝓘⁰ℍκ⨁⌊⌋𝟭𝕎θᵀ─χρξᗮë⨯ᵇ⊣↥Δ𝒥ℬ⅟∙◃⊞≺ₖ⇒ₕ₅⌈⌉│⊂∠≼ℱ⨿ℓ○ᵤⁱ⊚⨂ⁿ”“₋ϖ⋊ᘁ⁺𝒄↓₆ₚᴴΩ𝒞–«»‖₇ℰä⊇₈𝒟𝒯𝓢Čò𝓡ⱼ⊙†↾Ιυ§²𝒰∐⋯↿ôᾰ↟©◫𝒅𝒫∼𝑳ℵₒ…𝑹𝒮ăᵣ𝔭ɱ𝓚·𝒢ᵏ↻𝒪𝔮𝔽à′♯−↗∶⁴↠⌟┌├🎉çêőüℋ’⋁∋³<200c>⊹📋áí™⇐↘⊑½ᵈ⅓⇉∤✅❌èïł🛑µ‘💥⋆≰≻" | while read c; do echo -n "$c $(rg -o $c src | wc -l)\t"; rg $c src | head -n1; done
α 66486	src/tactic/fix_reflect_string.lean:meta instance {α} [has_reflect α] : has_reflect (thunk α) | a :=
λ 45242	src/model_theory/basic.lean:def empty : language := ⟨λ _, pempty, λ _, pempty⟩
→ 42292	src/model_theory/basic.lean:* A `first_order.language.hom`, denoted `M →[L] N`, is a map from the `L`-structure `M` to the
⟨ 35874	src/testing/slim_check/testable.lean:  shrink := λ ⟨x,y,h⟩, (λ ⟨x,y⟩, { x := x, y := x + y, h := /- proof -/}) <$> shrink (x, y - x)
⟩ 35874	src/model_theory/basic.lean:def empty : language := ⟨λ _, pempty, λ _, pempty⟩
₂ 29943	src/control/uliftable.lean:universes u₀ u₁ v₀ v₁ v₂ w w₀ w₁
₁ 29655	src/model_theory/basic.lean:⟨λ S₁ S₂,
β 23153	src/linear_algebra/unitary_group.lean:We also define the orthogonal group `orthogonal_group n β`, where `β` is a `comm_ring`.
← 18995	src/model_theory/basic.lean:    rw [← function.comp.assoc, equiv.to_fun_as_coe, equiv.self_comp_symm, function.comp.left_id]
≤ 15901	src/model_theory/basic.lean:{ le           := (≤),
∈ 15825	src/model_theory/basic.lean:∀ (x : fin n → M), (∀ i : fin n, x i ∈ s) → fun_map f x ∈ s
∀ 14589	src/model_theory/basic.lean:(empty_functions : ∀ n, L.functions n → false)
ℕ 12055	src/testing/slim_check/testable.lean:`∀ i j : ℕ, i ≤ j` has a `testable` instance because `ℕ` is sampleable
μ 10630	src/category_theory/enriched/basic.lean:  comp := λ (X Y Z : C), F.μ _ _ ≫ F.map (e_comp V X Y Z),
ι 10301	src/model_theory/basic.lean:lemma mem_infi {ι : Sort*} {S : ι → L.substructure M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i :=
ℝ 9806	src/probability_theory/integration.lean:  (c : ℝ≥0∞) {T : set α} (h_meas_T : measurable_set T)
∥ 9544	src/topology/continuous_function/bounded.lean:lemma norm_def : ∥f∥ = dist f 0 := rfl
↔ 9506	src/model_theory/basic.lean:(map_rel' : ∀{n} (r : L.relations n) x, rel_map r (to_fun ∘ x) ↔ rel_map r x . obviously)
𝕜 7892	src/measure_theory/measure/with_density_vector_measure.lean:@[simp] lemma with_densityᵥ_smul {𝕜 : Type*} [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E]
₀ 6351	src/measure_theory/function/lp_space.lean:    ↔ ∃ f₀ : (α →ᵇ E), f₀.to_continuous_map.to_ae_eq_fun μ = (f : α →ₘ[μ] E) :=
⁻ 5838	src/model_theory/basic.lean:{ carrier := (φ ⁻¹' S),
≠ 5357	src/testing/slim_check/testable.lean:instance ne.printable_prop {α} [has_repr α] (x y : α) : printable_prop (x ≠ y) :=
⟶ 5251	src/algebraic_topology/simplicial_set.lean:a morphism `Δ[n] ⟶ ∂Δ[n]`.
¹ 5099	src/model_theory/basic.lean:{ carrier := (φ ⁻¹' S),
∃ 4822	src/model_theory/basic.lean:  y ∈ S.map f ↔ ∃ x ∈ S, f x = y :=
≫ 4558	src/algebraic_topology/simplicial_set.lean:  map := λ m₁ m₂ f α, ⟨f.unop ≫ (α : Δ[n].obj m₁),
γ 4483	src/analysis/special_functions/integrals.lean:  have h : ∀ α β γ : ℝ, α * (β * α * γ) = β * (α * α * γ) := λ α β γ, by ring,
• 4412	src/tactic/abel.lean:def term {α} [add_comm_monoid α] (n : ℕ) (x a : α) : α := n • x + a
∧ 4226	src/model_theory/basic.lean:lemma mem_inf {p p' : L.substructure M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' := iff.rfl
× 4120	src/testing/slim_check/testable.lean:      then pure (⟨a, r, ⟨h⟩⟩ : (Σ a, test_result (β (interp α a)) × plift (sizeof_lt a x)))
≃ 4055	src/model_theory/basic.lean:* A `first_order.language.equiv`, denoted `M ≃[L] N`, is an equivalence from the `L`-structure `M`
Π 4011	src/system/random/basic.lean:(random_r : Π g [random_gen g] (x y : α),
ε 3748	src/analysis/specific_limits.lean:metric.mk_uniformity_basis (λ i _, pow_pos h₀ _) $ λ ε ε0,
σ 3620	src/meta/coinductive_predicates.lean:        do [(_,hs',σ)] ← cases_core h hs,
𝓝 3314	src/dynamics/omega_limit.lean:  ∀ n ∈ 𝓝 y, ∃ᶠ t in f, (s ∩ ϕ t ⁻¹' n).nonempty :=
ℤ 3270	src/testing/slim_check/testable.lean:tested. `α` is instantiated with `ℤ` first and then tested as normal
₃ 3261	src/testing/slim_check/sampleable.lean:    have h₃ : 0 < m,
⊆ 3244	src/model_theory/basic.lean:def closure : lower_adjoint (coe : L.substructure M → set M) := ⟨λ s, Inf {S | s ⊆ S},
φ 3024	src/model_theory/basic.lean:@[simp] lemma map_fun (φ : M →[L] N) {n : ℕ} (f : L.functions n) (x : fin n → M) :
↑ 2949	src/model_theory/basic.lean:lemma const_mem {c : L.const} : ↑c ∈ S :=
ₗ 2921	src/representation_theory/maschke.lean:variables (π : W →ₗ[k] V)
∞ 2926	src/probability_theory/integration.lean:  (c : ℝ≥0∞) {T : set α} (h_meas_T : measurable_set T)
≥ 2919	src/probability_theory/integration.lean:  (c : ℝ≥0∞) {T : set α} (h_meas_T : measurable_set T)
∘ 2904	src/model_theory/basic.lean:(map_fun' : ∀{n} (f : L.functions n) x, to_fun (fun_map f x) = fun_map f (to_fun ∘ x) . obviously)
π 2713	src/representation_theory/maschke.lean:and a `k[G]`-linear map `i : V → W` which admits a `k`-linear retraction `π`,
⥤ 2691	src/measure_theory/measure/giry_monad.lean:monad to an honest monad of the functor `Measure : Meas ⥤ Meas`.
∑ 2542	src/representation_theory/maschke.lean:∑ g : G, π.conjugate g
▸ 2182	src/model_theory/basic.lean:⟨λ h x, h ▸ rfl, λ h, ext h⟩
∩ 2139	src/model_theory/basic.lean:  closed_under f (s ∩ t) :=
⊤ 2019	src/model_theory/basic.lean:instance : inhabited (L.substructure M) := ⟨⊤⟩
δ 1978	src/testing/slim_check/sampleable.lean:    subtype.rec_on a $ λ δ h', ⟨⟨x + δ, nat.le_add_right _ _⟩, nat.add_lt_of_lt_sub_left h'⟩) <$>
∫ 1896	src/probability_theory/integration.lean:  ∫⁻ a, f a * T.indicator (λ _, c) a ∂μ = ∫⁻ a, f a ∂μ * ∫⁻ a, T.indicator (λ _, c) a ∂μ :=
∂ 1812	src/dynamics/ergodic/measure_preserving.lean:  (hgm : measurable (uncurry g)) (hg : ∀ᵐ x ∂μa, map (g x) μc = μd) :
¬ 1664	src/representation_theory/maschke.lean:familiar `¬(ring_char k ∣ fintype.card G)`. It is possible to convert between them using
⊓ 1622	src/model_theory/basic.lean:  closed_under f (s ⊓ t) := hs.inter ht
⊥ 1583	src/model_theory/basic.lean:@[simp] lemma closure_empty : closure L (∅ : set M) = ⊥ :=
Γ 1539	src/set_theory/zfc.lean:pSet.rec_on x $ λ α A IH y, pSet.cases_on y $ λ β B ⟨γ, Γ⟩ ⟨αβ, βα⟩ ⟨γβ, βγ⟩,
𝟙 1500	src/algebraic_topology/simplicial_object.lean:  X.σ i ≫ X.δ i.cast_succ = 𝟙 _ :=
⊔ 1422	src/model_theory/basic.lean:lemma closure_union (s t : set M) : closure L (s ∪ t) = closure L s ⊔ closure L t :=
∣ 1420	src/set_theory/ordinal_arithmetic.lean:theorem dvd_add_iff : ∀ {a b c : ordinal}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
⊗ 1399	src/control/functor/multivariate.lean:variables (p : α ⟹ repeat n Prop) (r : α ⊗ α ⟹ repeat n Prop)
ᶠ 1392	src/dynamics/omega_limit.lean:  {gb : β → β'} (hg : ∀ᶠ t in f, eq_on (gb ∘ (ϕ t)) (ϕ' t ∘ ga) s)
∏ 1382	src/probability_theory/independence.lean:  `μ (⋂ i in s, f i) = ∏ i in s, μ (f i) `. It will be used for families of π-systems.
ℂ 1324	src/tactic/norm_cast.lean:@[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n :=
∨ 1315	src/geometry/euclidean/circumcenter.lean:| (point_index i) := if i = i₁ ∨ i = i₂ then 1 else 0
ν 1286	src/probability_theory/independence.lean:  let ν := (μ t1) • μ,
∪ 1252	src/model_theory/basic.lean:lemma closure_union (s t : set M) : closure L (s ∪ t) = closure L s ⊔ closure L t :=
⋙ 1239	src/algebraic_topology/simplex_category.lean:    refine equiv.ulift.symm.trans (((skeletal_functor ⋙ forget _).map_iso I).to_equiv.trans _),
≅ 1131	src/algebra/homology/single.lean:def single_obj_X_self (j : ι) (A : V) : ((single V c j).obj A).X j ≅ A :=
ℚ 1109	src/testing/slim_check/sampleable.lean:instance rat.sampleable : sampleable ℚ :=
⋃ 1031	src/model_theory/basic.lean:lemma closure_Union {ι} (s : ι → set M) : closure L (⋃ i, s i) = ⨆ i, closure L (s i) :=
∅ 1022	src/model_theory/basic.lean:@[simp] lemma closure_empty : closure L (∅ : set M) = ⊥ :=
ᶜ 922	src/dynamics/omega_limit.lean:  let j := λ u, (closure (image2 ϕ (u ∩ v) s))ᶜ,
ₘ 919	src/geometry/manifold/diffeomorph.lean:* `M ≃ₘ^n⟮I, I'⟯ M'`  := `diffeomorph I J M N n`
ₐ 831	src/field_theory/splitting_field.lean:/-- If `p` is the minimal polynomial of `a` over `F` then `F[a] ≃ₐ[F] F[x]/(p)` -/
ᵥ 803	src/topology/list.lean:  tendsto (λp:α×vector α n, p.1 ::ᵥ p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a ::ᵥ l)) :=
ω 745	src/dynamics/omega_limit.lean:# ω-limits
ᵐ 729	src/dynamics/ergodic/measure_preserving.lean:  (hgm : measurable (uncurry g)) (hg : ∀ᵐ x ∂μa, map (g x) μc = μd) :
⨆ 726	src/model_theory/basic.lean:lemma closure_Union {ι} (s : ι → set M) : closure L (⋃ i, s i) = ⨆ i, closure L (s i) :=
⟪ 718	src/measure_theory/function/l1_space.lean:local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
⟫ 718	src/measure_theory/function/special_functions.lean:local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
∉ 714	src/testing/slim_check/functions.lean:  x ∉ xs → list.apply_id.{u} (xs.zip ys) x = x :=
⊢ 714	src/set_theory/ordinal_notation.lean:  simp [has_sub.sub, sub] at h' ⊢,
⦃ 695	src/model_theory/basic.lean:lemma ext ⦃f g : M →[L] N⦄ (h : ∀ x, f x = g x) : f = g :=
⦄ 695	src/model_theory/basic.lean:lemma ext ⦃f g : M →[L] N⦄ (h : ∀ x, f x = g x) : f = g :=
⨅ 691	src/model_theory/basic.lean:lemma mem_infi {ι : Sort*} {S : ι → L.substructure M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i :=
⁅ 690	src/ring_theory/derivation.lean:The notation `⁅D1, D2⁆` is used for the commutator of two derivations.
⁆ 690	src/ring_theory/derivation.lean:The notation `⁅D1, D2⁆` is used for the commutator of two derivations.
⊕ 673	src/ring_theory/noetherian.lean:If `M ⊕ N` embeds into `M`, for `M` noetherian over `R`, then `N` is trivial.
⇑ 666	src/model_theory/basic.lean:@[simp] theorem coe_subtype : ⇑S.subtype = coe := rfl
ᵖ 645	src/control/fold.lean:@[reducible] def foldl (α : Type u) : Type u := (End α)ᵒᵖ
τ 644	src/ring_theory/polynomial/symmetric.lean:+ `σ τ : Type*` (indexing the variables)
ᵒ 632	src/tactic/equiv_rw.lean:  -- The function arrow is technically a bifunctor `Typeᵒᵖ → Type → Type`,
⟦ 615	src/dynamics/circle/rotation_number/translation_number.lean:`⟦a⟧ = f 0`, where `⟦⟧` means the natural projection `ℝ → ℝ/ℤ`. Then there exists a unique
⟧ 615	src/dynamics/circle/rotation_number/translation_number.lean:`⟦a⟧ = f 0`, where `⟦⟧` means the natural projection `ℝ → ℝ/ℤ`. Then there exists a unique
ϕ 590	src/algebra/char_zero.lean:lemma ring_hom.char_zero (ϕ : R →+* S) [hS : char_zero S] : char_zero R :=
Σ 584	src/category_theory/preadditive/projective_resolution.lean:  Σ' g'' : P.complex.X (n+2) ⟶ Q.complex.X (n+2),
ᵢ 569	src/ring_theory/integral_closure.lean:  -- We can write `x` as `∑ rᵢ yᵢ` for `yᵢ ∈ Y`.
‹ 532	src/control/lawful_fix.lean:  apply @le_trans _ _ _ (approx f j_n) _ (j_ih ‹_›),
› 532	src/algebraic_topology/simplex_category.lean:  { exact (nat.succ_pred_eq_of_pos (lt_of_le_of_lt (zero_le _) ‹_›)).symm, },
ₙ 529	src/data/qpf/multivariate/constructions/prj.lean:functor `F` such that `F (α₀..αᵢ₋₁, αᵢ, αᵢ₊₁..αₙ₋₁) = αᵢ`
₄ 527	src/testing/slim_check/sampleable.lean:      have h₄ : xs₁ = xs.take k,
ₜ 522	src/dynamics/flow.lean:A subset `s` of `α` is invariant under a family of maps `ϕₜ : α → α`
Φ 520	src/topology/metric_space/hausdorff_distance.lean:{s t : set α} {Φ : α → β}
⋂ 493	src/model_theory/basic.lean:⟨λ s, { carrier := ⋂ t ∈ s, ↑t,
ψ 492	src/ring_theory/power_series/basic.lean:@[ext] lemma ext {φ ψ} (h : ∀ (n : σ →₀ ℕ), coeff R n φ = coeff R n ψ) :
ℒ 484	src/measure_theory/integral/integrable_on.lean:  refine mem_ℒp_one_iff_integrable.mp _,
𝕂 448	src/analysis/calculus/inverse.lean:`ℝ` or `ℂ` and implemented here assuming `is_R_or_C 𝕂`.
⬝ 444	src/combinatorics/simple_graph/adj_matrix.lean:  (G.adj_matrix α ⬝ M) v w = ∑ u in G.neighbor_finset v, M u w :=
ö 434	src/dynamics/fixed_points/topology.lean:Authors: Yury Kudryashov, Johannes Hölzl
↪ 432	src/model_theory/basic.lean:* A `first_order.language.embedding`, denoted `M ↪[L] N`, is an embedding from the `L`-structure `M`
η 425	src/control/traversable/instances.lean:variable (η : applicative_transformation F G)
𝓤 409	src/topology/sequences.lean:  (hU : is_countably_generated (𝓤 β)) :
𝓟 387	src/topology/local_extr.lean:have 𝓝 a ≤ 𝓟 s, from le_principal_iff.2 hs,
𝔸 359	src/analysis/calculus/deriv.lean:variables {𝕜' 𝔸 : Type*} [normed_field 𝕜'] [normed_ring 𝔸] [normed_algebra 𝕜 𝕜']
≈ 346	src/set_theory/game.lean:In this file we define the quotient of pre-games by the equivalence relation `p ≈ q ↔ p ≤ q ∧ q ≤
ₛ 339	src/measure_theory/measure/with_density_vector_measure.lean:the vector measure which maps the set `s` to `∫ₛ f ∂μ`. -/
⟮ 324	src/ring_theory/trace.lean:  algebra.trace K K⟮x⟯ (adjoin_simple.gen K x) = 0 :=
⟯ 324	src/ring_theory/trace.lean:  algebra.trace K K⟮x⟯ (adjoin_simple.gen K x) = 0 :=
Ψ 323	src/topology/metric_space/gluing.lean:  |Ψ
é 315	src/probability_theory/independence.lean:Copyright (c) 2021 Rémy Degenne. All rights reserved.
Λ 314	src/tactic/mk_iff_of_inductive_prop.lean:R as := ∃ bs, Λ_i a_i = p_i[bs]
₊ 301	src/measure_theory/function/l1_space.lean:  have : ∀ x, (∥(f x).to_real∥₊ : ℝ≥0∞) =
≡ 282	src/combinatorics/pigeonhole.lean:  ∃ (m ∈ s) (n ∈ s), m < n ∧ m ≡ n [MOD k] :=
↦ 267	src/set_theory/game/domineering.lean:/-- The embedding `(x, y) ↦ (x, y+1)`. -/
⟹ 263	src/control/functor/multivariate.lean:(map : Π {α β : typevec n}, (α ⟹ β) → (F α → F β))
≪ 253	src/ring_theory/noetherian.lean:  refine (f.tailing_linear_equiv i n).symm ≪≫ₗ _,
ζ 251	src/ring_theory/roots_of_unity.lean:* `is_primitive_root ζ k`: an element `ζ` is a primitive `k`-th root of unity if `ζ ^ k = 1`,
ᵃ 241	src/linear_algebra/affine_space/midpoint.lean:@[simp] lemma affine_map.map_midpoint (f : P →ᵃ[R] P') (a b : P) :
≌ 231	src/algebraic_topology/simplicial_object.lean:def simplicial_cosimplicial_equiv : (simplicial_object C)ᵒᵖ ≌ (cosimplicial_object Cᵒᵖ) :=
√ 219	src/number_theory/lucas_lehmer.lean:/-- We construct the ring `X q` as ℤ/qℤ + √3 ℤ/qℤ. -/
𝓘 215	src/geometry/manifold/diffeomorph.lean:* `E ≃ₘ^n[𝕜] E'`      := `E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'`
⁰ 213	src/ring_theory/non_zero_divisors.lean:This file declares the notation `R⁰` for the submonoid of non-zero-divisors of `R`,
ℍ 209	src/linear_algebra/clifford_algebra/equivs.lean:as an `R`-algebra to `ℍ[R,c₁,c₂]`. -/
κ 202	src/data/set/finite.lean:lemma finite.pi {δ : Type*} [fintype δ] {κ : δ → Type*} {t : Π d, set (κ d)}
⨁ 196	src/ring_theory/polynomial/homogeneous.lean:* show that `mv_polynomial σ R ≃ₐ[R] ⨁ i, homogeneous_submodule σ R i`
⌊ 195	src/dynamics/circle/rotation_number/translation_number.lean:We prove the estimates `f 0 + ⌊g 0⌋ ≤ f (g 0) ≤ f 0 + ⌈g 0⌉` and some corollaries with added/removed
⌋ 195	src/number_theory/class_number/admissible_abs.lean:  have hi : (⌊↑(A i₀ % b) / abs b • ε⌋.nat_abs : ℤ) = ⌊↑(A i₁ % b) / abs b • ε⌋.nat_abs :=
𝟭 194	src/topology/category/Top/opens.lean:`map_id : map (𝟙 X) ≅ 𝟭 (opens X)` and
𝕎 190	src/ring_theory/witt_vector/identities.lean:local notation `𝕎` := witt_vector p -- type as `\bbW`
θ 186	src/set_theory/cofinality.lean:theorem infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : cardinal) (hθ : θ ≤ #β)
ᵀ 175	src/combinatorics/simple_graph/adj_matrix.lean:  (G.adj_matrix α)ᵀ = G.adj_matrix α :=
─ 171	src/category_theory/triangulated/pretriangulated.lean:    X  ───> Y  ───> Z  ───> X⟦1⟧
χ 168	src/ring_theory/witt_vector/is_poly.lean:    obtain ⟨χ, hh⟩ := hh },
ρ 166	src/control/monad/basic.lean:  {α₁ ρ₁ : Type u₀} {α₂ ρ₂ : Type u₁} (F : (ρ₁ → m₁ α₁) ≃ (ρ₂ → m₂ α₂)) :
ξ 158	src/ring_theory/roots_of_unity.lean:  mul_mem' := λ ζ ξ hζ hξ, by simp only [*, set.mem_set_of_eq, mul_pow, one_mul] at *,
ᗮ 149	src/geometry/euclidean/monge_point.lean:  (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
ë 148	src/combinatorics/composition.lean:Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
⨯ 145	src/category_theory/is_connected.lean:This allows us to show that the functor X ⨯ - preserves connected limits.
ᵇ 143	src/topology/continuous_function/bounded.lean:localized "infixr ` →ᵇ `:25 := bounded_continuous_function" in bounded_continuous_function
⊣ 143	src/algebraic_topology/simplicial_set.lean:noncomputable def sSet_Top_adj : sSet.to_Top ⊣ Top.to_sSet :=
↥ 132	src/dynamics/flow.lean:def restrict {s : set α} (h : is_invariant ϕ s) : flow τ ↥s :=
Δ 122	src/order/symm_diff.lean:* `a Δ b`: `symm_diff a b`
𝒥 120	src/topology/category/Top/limits.lean:{ has_limits_of_shape := λ J 𝒥, by exactI
ℬ 113	src/category_theory/monoidal/of_chosen_finite_products.lean:variables (ℬ : Π (X Y : C), limit_cone (pair X Y))
⅟ 108	src/representation_theory/maschke.lean:⅟(fintype.card G : k) • (π.sum_of_conjugates_equivariant G)
∙ 108	src/ring_theory/noetherian.lean:theorem fg_span_singleton (x : M) : fg (R ∙ x) :=
◃ 108	src/algebra/quandle.lean:* `x ◃ y` is `shelf.act x y`
⊞ 104	src/category_theory/preadditive/projective.lean:  projective (P ⊞ Q) :=
≺ 103	src/testing/slim_check/sampleable.lean:local infix ` ≺ `:50 := has_well_founded.r
ₖ 100	src/combinatorics/composition.lean:/-- Given a list of length `n` and a composition `[i₁, ..., iₖ]` of `n`, split `l` into a list of
⇒ 98	src/tactic/transfer.lean:bound by `S` are called arguments. `R` is generally constructed using `⇒` (i.e. `relator.lift_fun`).
ₕ 96	src/geometry/manifold/instances/sphere.lean:(stereographic (norm_eq_of_mem_sphere v)) ≫ₕ
₅ 92	src/testing/slim_check/sampleable.lean:      have h₅ : ∀ (a : list α), sizeof_lt a xs₂ → sizeof_lt (xs₁ ++ a) xs,
⌈ 91	src/dynamics/circle/rotation_number/translation_number.lean:We prove the estimates `f 0 + ⌊g 0⌋ ≤ f (g 0) ≤ f 0 + ⌈g 0⌉` and some corollaries with added/removed
⌉ 91	src/dynamics/circle/rotation_number/translation_number.lean:We prove the estimates `f 0 + ⌊g 0⌋ ≤ f (g 0) ≤ f 0 + ⌈g 0⌉` and some corollaries with added/removed
│ 81	src/tactic/explode.lean:    let margin := string.join (list.repeat " │" en.depth),
⊂ 81	src/order/zorn.lean:def super_chain (c₁ c₂ : set α) : Prop := chain c₂ ∧ c₁ ⊂ c₂
∠ 77	src/geometry/euclidean/sphere.lean:  (hapb : ∠ a p b = π) (hcpd : ∠ c p d = π) :
≼ 77	src/order/directed.lean:local infix ` ≼ ` : 50 := r
ℱ 76	src/topology/sheaves/stalks.lean:on the stalks `(f _* ℱ).stalk (f x) ⟶ ℱ.stalk x`.
⨿ 75	src/category_theory/preadditive/projective.lean:  projective (P ⨿ Q) :=
ℓ 75	src/topology/metric_space/kuratowski.lean:Any separable metric space can be embedded isometrically in `ℓ^∞(ℝ)`.
○ 75	src/topology/sequences.lean:  obtain ⟨W, W_in, hWW⟩ : ∃ W ∈ 𝓤 β, W ○ W ⊆ V n₀,
ᵤ 74	src/ring_theory/unique_factorization_domain.lean:local infix ` ~ᵤ ` : 50 := associated
ⁱ 71	src/group_theory/specific_groups/quaternion.lean:The identity `1` is given by `aⁱ`.
⊚ 70	src/control/functor/multivariate.lean:                    (h ⊚ g) <$$> x = h <$$> g <$$> x)
⨂ 68	src/linear_algebra/pi_tensor_product.lean:semirings. We denote this space by `⨂[R] i, s i` and define it as `free_add_monoid (R × Π i, s i)`
ⁿ 67	src/group_theory/sylow.lean:  prime power `pⁿ` dividing `G`, there exists a subgroup of `G` of order `pⁿ`.
” 66	src/dynamics/periodic_pts.lean:We provide “dot syntax”-style operations on terms of the form `h : is_periodic_pt f n x` including
“ 65	src/dynamics/periodic_pts.lean:We provide “dot syntax”-style operations on terms of the form `h : is_periodic_pt f n x` including
₋ 64	src/tactic/generalizes.lean:`kᵢ : Jᵢ[jᵢ₋₁ := kᵢ₋₁]...[j₀ := k₀]`.
ϖ 63	src/ring_theory/discrete_valuation_ring.lean:theorem irreducible_iff_uniformizer (ϖ : R) :
⋊ 62	src/group_theory/semidirect_product.lean:There are two homs into the semidirect product `inl : N →* N ⋊[φ] G` and
ᘁ 54	src/algebra/star/basic.lean:`r^*`, `r†`, `rᘁ`, and so on.
⁺ 53	src/dynamics/flow.lean:cases where `τ` is one of `ℕ`, `ℤ`, `ℝ⁺`, or `ℝ`, we use additive
𝒄 51	src/order/omega_complete_partial_order.lean: * `continuous_hom` (with notation →𝒄)
↓ 51	src/topology/dense_embedding.lean:g↓     ↓e
₆ 50	src/group_theory/specific_groups/cyclic.lean:      have hk₆ : (k % (nat.find hex : ℤ)).nat_abs = 0,
ₚ 48	src/ring_theory/power_series/well_known.lean:  It is given by `∑ n, x ^ n /ₚ u ^ (n + 1)`.
ᴴ 44	src/linear_algebra/matrix/circulant.lean:  (circulant v)ᴴ = circulant (star (λ i, v (-i))) :=
Ω 43	src/number_theory/arithmetic_function.lean: * `Ω n` is the number of prime factors of `n` counted with multiplicity.
𝒞 38	src/category_theory/enriched/basic.lean:def category_of_enriched_category_Type (C : Type u₁) [𝒞 : enriched_category (Type v) C] :
– 38	src/tactic/omega/find_scalars.lean:Tactic for performing Fourier–Motzkin elimination to find
« 37	src/tactic/interactive.lean:  «have» h q₁ q₂,
» 37	src/tactic/cache.lean:  «have» (some h) q₁ q₂,
‖ 32	src/data/fintype/card_embedding.lean:local notation `‖` x `‖` := fintype.card x
₇ 32	src/data/pnat/xgcd.lean:  { have h₇ : (gcd a b : ℕ) ∣ (gcd_z a b) * a :=
ℰ 31	src/category_theory/sites/sieves.lean:  Sup_le       := λ ℰ S hS Y f, by { rintro ⟨R, hR, hf⟩, apply hS R hR _ hf },
ä 30	src/combinatorics/hales_jewett.lean:Copyright (c) 2021 David Wärn. All rights reserved.
⊇ 30	src/topology/separation.lean:  (hV : directed (⊇) V) (hV_cpct : ∀ i, is_compact (V i)) {U : set α}
₈ 29	src/data/pnat/xgcd.lean:    have h₈ : (gcd a b : ℕ) ∣ (gcd_x a b) * b :=
𝒟 29	src/order/ideal.lean:- `order.ideal_of_cofinals p 𝒟`, where `p : P`, and `𝒟` is a countable family of cofinal
𝒯 28	src/category_theory/monoidal/of_chosen_finite_products.lean:variables (𝒯 : limit_cone (functor.empty C))
𝓢 28	src/topology/uniform_space/separation.lean:More generally, the intersection `𝓢 X` of all entourages of `X`, which has type `set (X × X)` is an
Č 27	src/algebraic_topology/cech_nerve.lean:# The Čech Nerve
ò 27	src/data/bundle.lean:Copyright © 2021 Nicolò Cavalleri. All rights reserved.
𝓡 26	src/geometry/manifold/smooth_manifold_with_corners.lean:  `n`-dimensional real manifolds without boundary (with notation `𝓡 n` in the locale `manifold`)
ⱼ 25	src/tactic/linarith/frontend.lean:`Rᵢ ∈ {<, ≤, =}` and each `tᵢ` is of the form `∑ cⱼxⱼ`.
⊙ 25	src/data/matrix/hadamard.lean:* `⊙`: the Hadamard product `matrix.hadamard`;
† 23	src/data/complex/is_R_or_C.lean:local postfix `†`:100 := @is_R_or_C.conj K _
↾ 21	src/category_theory/types.lean:as well as a corresponding notation `↾ f`. (Entered as `\upr `.) The notation is enabled using
Ι 20	src/measure_theory/integral/interval_integral.lean:  (∀ᵐ x ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ x ∂μ, x ∈ Ioc a b → P x) ∧ (∀ᵐ x ∂μ, x ∈ Ioc b a → P x) :=
υ 20	src/data/mv_polynomial/monad.lean:lemma bind₁_bind₁ {υ : Type*} (f : σ → mv_polynomial τ R) (g : τ → mv_polynomial υ R)
§ 19	src/ring_theory/noetherian.lean:([samuel, § 3.3, Lemma 3])-/
² 18	src/control/fold.lean:`xs ++ [x]` which would yield a `O(n²)` run time. -/
𝒰 17	src/topology/sheaves/sheaf_condition/equalizer_products.lean:variables (𝒰 : ι → opens V)
∐ 17	src/category_theory/graded_object.lean:{ obj := λ X, ∐ (λ i : ulift.{v} β, X i.down),
⋯ 16	src/tactic/wlog.lean:  `⊢ p xs_0 ∨ ⋯ ∨ p xs_n`
↿ 16	src/topology/path_connected.lean:  {a b : ι → X} (γ : Π (t : ι), path (a t) (b t)) (h : continuous ↿γ) :
ô 14	src/analysis/calculus/lhopital.lean:# L'Hôpital's rule for 0/0 indeterminate forms
ᾰ 13	src/meta/expr.lean:gives it the name `ᾰ`:
↟ 13	src/algebra/category/Module/subobject.lean:    refine ⟨λ h, _, λ h, mk_le_mk_of_comm ↟(submodule.of_le h) (by { ext, refl })⟩,
© 13	src/topology/vector_bundle.lean:Copyright © 2020 Nicolò Cavalleri. All rights reserved.
◫ 12	src/category_theory/functor_category.lean:infix ` ◫ `:80 := hcomp
𝒅 12	src/geometry/manifold/derivation_bundle.lean:localized "notation `𝒅` := fdifferential" in manifold
𝒫 12	src/data/set/function.lean:lemma inj_on_preimage {B : set (set β)} (hB : B ⊆ 𝒫 (range f)) :
∼ 11	src/group_theory/monoid_localization.lean:satisfying '`∀ y ∈ S`, `(1, 1) ∼ (y, y)` under `s`', we have that `(x₁, y₁) ∼ (x₂, y₂)` by `s`
𝑳 10	src/geometry/manifold/algebra/left_invariant_derivation.lean:lemma comp_L : (X f).comp (𝑳 I g) = X (f.comp (𝑳 I g)) :=
ℵ 10	src/set_theory/cardinal_ordinal.lean:  `aleph' n = n`, `aleph' ω = cardinal.omega = ℵ₀`, `aleph' (ω + 1) = ℵ₁`, etc.
ₒ 9	src/tactic/induction.lean:       (eq₁ : y₁ = z₁) ... (eqₖ : yₒ = zₒ), P
… 9	src/tactic/wlog.lean:  -- reorder s.t. context is Γ ⬝ vars ⬝ cases ⊢ ∀deps, …
𝑹 8	src/geometry/manifold/algebra/monoid.lean:Lemmas involving `smooth_right_mul` with the notation `𝑹` usually use `R` instead of `𝑹` in the
𝒮 8	src/category_theory/essentially_small.lean:  { rintro ⟨S, 𝒮, ⟨f⟩⟩,
ă 8	src/order/compactly_generated.lean:- [G. Călugăreanu, *Lattice Concepts of Module Theory*][calugareanu]
ᵣ 7	src/tactic/solve_by_elim.lean:* `solve_by_elim [h₁, h₂, ..., hᵣ]` also applies the named lemmas.
𝔭 7	src/algebraic_geometry/structure_sheaf.lean:$s : U → ⨆_{𝔭 ∈ U} A_𝔭$, such that $s(𝔭) ∈ A_𝔭$ for each $𝔭$,
É 7	src/dynamics/circle/rotation_number/translation_number.lean:  circle_deg1_lift`. This is a version of Proposition 5.4 from [Étienne Ghys, Groupes
± 7	src/order/filter/at_top_bot.lean:Then we prove many lemmas like “if `f → +∞`, then `f ± c → +∞`”.
𝓚 6	src/data/complex/is_R_or_C.lean:local notation `𝓚` := algebra_map ℝ _
· 6	src/analysis/normed_space/inner_product.lean:We globally denote the real and complex inner products by `⟪·, ·⟫_ℝ` and `⟪·, ·⟫_ℂ` respectively.
𝒢 5	src/topology/sheaves/presheaf.lean:def pushforward_map {X Y : Top.{v}} (f : X ⟶ Y) {ℱ 𝒢 : X.presheaf C} (α : ℱ ⟶ 𝒢) :
ᵏ 4	src/analysis/analytic/basic.lean:`Σ pₖ xᵏ` for `k ∈ {0,..., n-1}`. -/
↻ 4	src/category_theory/action.lean:From a multiplicative action M ↻ X, we can construct a functor from M to the category of
𝒪 4	src/algebraic_geometry/structure_sheaf.lean:For an open set $U ⊆ Spec A$, we define $𝒪(U)$ to be the set of functions
𝔮 4	src/algebraic_geometry/structure_sheaf.lean:contained in $U$, and elements $a, f ∈ A$, such that for each $𝔮 ∈ V, f ∉ 𝔮$,
𝔽 4	src/number_theory/class_number/admissible_absolute_value.lean:   mapping `p : polynomial 𝔽_q` to `q ^ degree p`, is admissible
à 4	src/set_theory/pgame.lean:* [André Joyal, *Remarques sur la théorie des jeux à deux personnes*][joyal1997]
′ 4	src/set_theory/zfc.lean:infixl `′`:100 := fval
♯ 4	src/data/pfunctor/univariate/M.lean:local prefix `♯`:0 := cast (by simp [*] <|> cc <|> solve_by_elim)
− 4	src/control/traversable/lemmas.lean:    In Journal of Functional Programming. Vol. 19. No. 3&4. Pages 377−402. 2009.
↗ 4	src/category_theory/sites/sheaf_of_types.lean:   ↓  ↗
∶ 4	src/algebra/pointwise.lean:/-- The scaling of a set `(x • s : set β)` by a scalar `x ∶ α` is defined as `{x • y | y ∈ s}`
⁴ 3	src/data/mv_polynomial/variables.lean:  For example if `p = x⁴y+yz` then `vars p = {x, y, z}`
↠ 3	src/category_theory/isomorphism.lean:Presumably we could write `X ↪ Y` and `X ↠ Y`.
⌟ 3	src/ring_theory/ideal/operations.lean:   v     \⌟
┌ 3	src/tactic/explode.lean:      | status.intro := " │" ++ margin ++ " ┌"
├ 3	src/tactic/explode.lean:      | status.sintro := " ├" ++ margin
🎉 3	src/tactic/interactive_expr.lean:The "goals accomplished 🎉" HTML widget. This can be overridden using:
ç 3	src/analysis/complex/isometry.lean:Copyright (c) 2021 François Sunatori. All rights reserved.
ê 3	src/number_theory/padics/padic_integers.lean:* [F. Q. Gouêva, *p-adic numbers*][gouvea1997]
ő 3	src/topology/category/Top/limits.lean:## Topological Kőnig's lemma
ü 3	src/ring_theory/witt_vector/teichmuller.lean:# Teichmüller lifts
ℋ 3	src/category_theory/fully_faithful.lean:lemma faithful.of_comp_iso {H : C ⥤ E} [ℋ : faithful H] (h : F ⋙ G ≅ H) : faithful F :=
’ 3	src/geometry/euclidean/sphere.lean:* `mul_dist_add_mul_dist_eq_mul_dist_of_cospherical`: Ptolemy’s Theorem (Freek No. 95).
⋁ 3	src/tactic/mk_iff_of_inductive_prop.lean:The new rule `r` has the shape `∀ps is, i as ↔ ⋁_j, ∃cs, is = cs`, where `ps` are the type
∋ 3	src/topology/paracompact.lean:  { /- For each `x ∈ s` we choose open disjoint `u x ∋ x` and `v x ⊇ t`. The sets `u x` form an
³ 2	src/data/mv_polynomial/variables.lean:  For example if `7 ≠ 0` in `R` and `p = x²y+7y³` then `degrees p = {x, x, y, y, y}`
 2	src/data/list/defs.lean:`aᵢ ∈ as` and `bᵢ ‌∈ bs`. If `bs` is shorter than `as`, `f` is applied to `none`
⊹ 2	src/tactic/localized.lean:localized "infix ` ⊹ `:60 := my_add" in my.add
📋 2	src/tactic/explode_widget.lean:                       attr.val "title" "copy expression to clipboard"] ["📋"],
á 2	src/topology/algebra/localization.lean:Copyright (c) 2021 María Inés de Frutos-Fernández. All rights reserved.
í 2	src/topology/algebra/localization.lean:Copyright (c) 2021 María Inés de Frutos-Fernández. All rights reserved.
™ 1	src/analysis/convex/exposed.lean:Generalise to Locally Convex Topological Vector Spaces™
⇐ 2	src/tactic/scc.lean:- if `pᵢ` is a root: `"pᵢ ⇐ i"`, where `i` is the preorder number of `pᵢ`,
↘ 2	src/category_theory/adjunction/mates.lean:    G ↓  ↗  ↓ H         G ↓  ↘  ↓ H
⊑ 2	src/tactic/monotonicity/interactive.lean:`ac_mono` reduces the `f x ⊑ f y`, for some relation `⊑` and a
½ 1	src/algebra/invertible.lean:invertible, inverse element, inv_of, a half, one half, a third, one third, ½, ⅓
ᵈ 1	src/analysis/convex/caratheodory.lean:in `ℝᵈ` is the union of the convex hulls of the `(d+1)`-tuples in `s`.
⅓ 1	src/algebra/invertible.lean:invertible, inverse element, inv_of, a half, one half, a third, one third, ½, ⅓
⇉ 1	src/category_theory/limits/shapes/split_coequalizer.lean:    X ⇉ Y → Z
∤ 1	src/tactic/omega/eq_elim.lean:| (nondiv i) := i.repr ++ "∤"
✅ 1	src/tactic/solve_by_elim.lean:  solve_by_elim_trace n (format!"✅ `{pp}` solves `⊢ {g}`")
❌ 1	src/tactic/solve_by_elim.lean:solve_by_elim_trace n (format!"❌ failed to solve `⊢ {g}`")
è 1	src/algebraic_geometry/EllipticCurve.lean:53-56 of [P. Deligne, *Courbes elliptiques: formulaire d'après J. Tate*][deligne_formulaire].
ï 1	src/analysis/calculus/times_cont_diff.lean:With a naïve direct definition, the `n`-th derivative of a function belongs to the space
ł 1	src/geometry/euclidean/monge_point.lean:* Małgorzata Buba-Brzozowa, [The Monge Point and the 3(n+1) Point
🛑 1	src/tactic/solve_by_elim.lean:      solve_by_elim_trace opt.max_depth "🛑 aborting, hit depth limit" >> failed),
µ 1	src/measure_theory/constructions/pi.lean:/-- If one of the measures `μ i` has no atoms, them `measure.pi µ`
‘ 1	src/topology/paracompact.lean:/- Dieudonné‘s theorem: a paracompact Hausdorff space is normal. Formalization is based on the proof
💥 1	src/tactic/explode_widget.lean:      attr.val "title" "explode"] ["💥"]]
⋆ 1	src/analysis/normed_space/inner_product.lean:local postfix `⋆`:90 := complex.conj
≰ 1	src/algebra/continued_fractions/convergents_equiv.lean:    { exact (m'.not_succ_le_zero m_le_n).elim }, -- 1 ≰ 0
≻ 1	src/tactic/omega/eq_elim.lean:| (reduce n) := "≻" ++ n.repr